Commit 2024-04-12 09:10 6888b634

chore: move FiniteDimensional.trans higher up the import hierarchy (#12079) @YaelDillies pointed out that the import Data.Complex.Module → FieldTheory.Tower brings with it too many things. The only declaration from FieldTheory.Tower needed for Data.Complex.Module is FiniteDimensional.trans, which we can easily move up the import hierarchy (14 imports higher, in fact). So this means we can cut the long pole of Mathlib by up to 13 files. Specific Zulip discussion starts here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432796670