Commit 2026-08-05 23:02 6dba1823

View on Github →

feat(Algebra/Polynomial/Degree): add variation of degree_sub_lt (#41214)

Add _right variation of Polynomial.degree_sub_lt.
Rename Polynomial.degree_sub_lt to Polynomial.degree_sub_lt_left

Estimated changes

Modified Mathlib/Algebra/Polynomial/Degree/Defs.lean

deleted theorem Polynomial.degree_sub_lt

added theorem Polynomial.degree_sub_lt_left

added theorem Polynomial.degree_sub_lt_right

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Algebra/Polynomial/Sequence.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean