Theorem AddSubgroup.relindex_eq_abs_det

Modification history

2025-09-13 17:16
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
chore(GroupTheory/Index): rename `relindex` to `relIndex` (#19872) …
Deleted AddSubgroup.relindex_eq_abs_detView on Github →
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 →