Commit 2025-03-16 07:15 f988aaba

View on Github →

feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940)

Estimated changes

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Basis.addSubgroupOfClosure_apply

added theorem Basis.addSubgroupOfClosure_repr_apply

Modified Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean

added theorem AddSubgroup.index_eq_natAbs_det

deleted theorem AddSubgroup.natAbs_det_basis_change

added theorem AddSubgroup.relindex_eq_abs_det

added theorem AddSubgroup.relindex_eq_natAbs_det