Theorem AddSubgroup.natAbs_det_basis_change

Modification history

2025-03-16 07:15
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940)
Deleted AddSubgroup.natAbs_det_basis_changeView on Github →
2025-03-14 10:49
Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean
refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank (#22902) …
Added AddSubgroup.natAbs_det_basis_changeView on Github →