Theorem Matrix.discr_conj

Modification history

2026-05-13 03:36
Mathlib/LinearAlgebra/Matrix/Charpoly/Disc.lean
feat(UpperHalfPlane): define PGL action on the upper half-plane (#36330)
Modified Matrix.discr_conjView on Github →
2025-10-20 10:08
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
chore: change `disc` to `discr` to denote the discriminant (#30709) …
Added Matrix.discr_conjView on Github →