Theorem AddSubgroup.index_eq_natAbs_det

Modification history

2025-03-16 07:15
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940)
Added AddSubgroup.index_eq_natAbs_detView on Github →