Theorem finrank_quotient_torsion_eq

Modification history

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