Theorem finrank_quotient_eq_of_le_torsion

Modification history

2026-06-07 01:53
Mathlib/LinearAlgebra/Dimension/Torsion/Basic.lean
feat: add NumberField.Units.finrank_eq (#40239) …
Added finrank_quotient_eq_of_le_torsionView on Github →