Def Matrix.GeneralLinearGroup.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.upperRightHom View on Github →