lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)

Commit

4 years ago

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

Author

pechersky

Parents

c4caf0ee

mathlib3 fdf09df0 - feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)

mathlib3
fdf09df0 - feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)