Theorem Polynomial.exists_eval_eq_iff

Modification history

2026-04-21 14:07
Mathlib/LinearAlgebra/Lagrange.lean
feat: a Lie module with trivial trace form is nilpotent over the derived subalgebra (#37622) …
Added Polynomial.exists_eval_eq_iffView on Github →