Mathlib dependencies

The single funnel for Mathlib imports: every module of this tree imports Mathlib through this file only, so the development's Mathlib footprint is auditable at a glance.