Commit 2026-11-10 14:51 21fc68be

View on Github →

feat(LinearAlgebra/Matrix): add the prodEquiv for Matrix, GL and SL (#44876)

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

modified def Matrix.piAddEquiv

modified def Matrix.piAlgEquiv

modified def Matrix.piLinearEquiv

modified def Matrix.piRingEquiv

added def Matrix.prodAddEquiv

added def Matrix.prodAlgEquiv

added def Matrix.prodEquiv

added def Matrix.prodLinearEquiv

added def Matrix.prodRingEquiv

added theorem Matrix.toAddEquiv_piLinearEquiv

added theorem Matrix.toAddEquiv_piRingEquiv

added theorem Matrix.toAddEquiv_prodLinearEquiv

added theorem Matrix.toAddEquiv_prodRingEquiv

added theorem Matrix.toAddEquiv_transposeLinearEquiv

added theorem Matrix.toEquiv_piAddEquiv

added theorem Matrix.toEquiv_prodAddEquiv

added theorem Matrix.toLinearEquiv_piAlgEquiv

added theorem Matrix.toLinearEquiv_prodAlgEquiv

added theorem Matrix.toRingEquiv_piAlgEquiv

added theorem Matrix.toRingEquiv_prodAlgEquiv

added theorem Matrix.toRingEquiv_transposeAlgEquiv

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

added theorem Matrix.det_prodRingEquiv_symm

added theorem Matrix.fst_det

added theorem Matrix.snd_det

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

added def Matrix.GeneralLinearGroup.prodEquiv

added theorem Matrix.GeneralLinearGroup.prodEquiv_apply

added theorem Matrix.GeneralLinearGroup.val_prodEquiv_symm_apply

Modified Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean

added def Matrix.SpecialLinearGroup.prodEquiv