Theorem Matrix.sub_scalar_sq_eq_discr

Modification history

2025-10-20 10:08
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
chore: change `disc` to `discr` to denote the discriminant (#30709) …
Added Matrix.sub_scalar_sq_eq_discrView on Github →