Commit 2024-11-07 23:00 dfe98ef4
View on Github →chore(LinearAlgebra/Dimension): split off rank_quotient_eq_of_le_torsion (#18730)
This result doesn't seem to be used in Mathlib and it pulls in many imports such as the theory of the ring ZMod, which we should not need to define finite dimensional spaces.