Theorem Matrix.GeneralLinearGroup.val_prodEquiv_symm_apply

Modification history

2026-11-10 14:51

Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

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

Added Matrix.GeneralLinearGroup.val_prodEquiv_symm_apply View on Github →