Theorem NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zero

Modification history

2025-11-05 14:53
Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean
feat(Analysis/Normed/Algebra/GelfandMazur): new file (#29649) …
Added NormedAlgebra.Real.exists_isMonicOfDegree_two_and_aeval_eq_zeroView on Github →