Commit 2024-08-21 22:09 4dbcdfc3

View on Github →

feat(Polynomial): natDegree_add_eq_left_of_degree_lt (#16031)

Estimated changes

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

added theorem Polynomial.natDegree_add_eq_left_of_degree_lt

added theorem Polynomial.natDegree_add_eq_right_of_degree_lt