Theorem Matrix.GeneralLinearGroup.injective_upperRightHom

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.injective_upperRightHomView on Github →