Commit 2026-02-12 11:04 95f7066a

View on Github →

chore(Charpoly/Disc): use nontriviality to drop a Nontrivial assumption (#35117)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Disc.lean

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

modified theorem Matrix.GeneralLinearGroup.isParabolic_conj_iff'

modified theorem Matrix.GeneralLinearGroup.isParabolic_conj_iff