Theorem Polynomial.normUnit_X

Modification history

2026-07-08 15:11

Mathlib/Algebra/Polynomial/FieldDivision.lean

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

Modified Polynomial.normUnit_X 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.normUnit_X View on Github →