Theorem Algebra.aeval_self_charpoly_lmul

Modification history

2026-04-15 19:09
Mathlib/LinearAlgebra/Charpoly/Basic.lean
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) …
Added Algebra.aeval_self_charpoly_lmulView on Github →