Theorem Polynomial.X_eq_normalize

Modification history

2026-07-08 15:11

Mathlib/Algebra/Polynomial/FieldDivision.lean

refactor(Algebra): weaken NormalizationMonoid (#34179) …

Modified Polynomial.X_eq_normalize View on Github →

2024-03-27 19:08

Mathlib/Data/Polynomial/FieldDivision.lean

feat(Data/Polynomial/FieldDivision): add two lemmas about normalization of X (#11720) …

Added Polynomial.X_eq_normalize View on Github →