Theorem Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det

Modification history

2025-10-15 06:00
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
feat(GeneralLinearGroup/FinTwo): the addChar sending x to [1,x;0,1] (#30475)
Added Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_detView on Github →