Theorem AddSubgroup.relindex_eq_abs_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.relindex_eq_abs_detView on Github →