Commit 2021-12-31 19:13 fdf09df0

View on Github →

feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121) Also two helper lemmas on nat_degree. Generalize degree_sum_fin_lt to semirings

Estimated changes

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.nat_degree_add_eq_left_of_nat_degree_lt

added theorem polynomial.nat_degree_add_eq_right_of_nat_degree_lt

Modified src/data/polynomial/degree/lemmas.lean

added theorem polynomial.degree_sum_eq_of_disjoint

added theorem polynomial.nat_degree_sum_eq_of_disjoint