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) …
Added AddSubgroup.relIndex_eq_abs_detView on Github →