Commit 2024-03-27 19:08 b3744d54

View on Github →

feat(Data/Polynomial/FieldDivision): add two lemmas about normalization of X (#11720) Add two lemmas normUnit_X and X_eq_normalize on the normalization unit for the monoid X.

Estimated changes

added theorem Polynomial.normUnit_X