Theorems · Theorem · field theory

Polynomial.degree_sum_eq_of_disjoint

∀ {R : Type u} {S : Type v} [inst : Semiring R] (f : S → Polynomial R) (s : Finset S),
  {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.degree ∘ f)) →
    (s.sum f).degree = s.sup fun i => (f i).degree

Defined in

Mathlib.Algebra.Polynomial.Degree.Lemmas

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring