Commit 2026-02-10 22:14 b77ed640

View on Github →

feat(GeneralLinearGroup): define GeneralLinearGroup.scalar (#34986) I'm going to use it in lemmas about PGL(n, R), see #34987.

Estimated changes

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

added theorem Matrix.GeneralLinearGroup.center_eq_range_scalar

deleted theorem Matrix.GeneralLinearGroup.center_eq_range_units

deleted theorem Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar

added theorem Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar

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

added theorem Matrix.GeneralLinearGroup.det_scalar

added def Matrix.GeneralLinearGroup.scalar

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