Theorems · Theorem · field theory

Polynomial.degree_sum_eq_of_linearIndepOn

∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommRing R] {A : Type u_1} [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {f : ι → Polynomial R} {v : ι → A},
  LinearIndepOn R v ↑s → (∑ i ∈ s, v i • Polynomial.map (algebraMap R A) (f i)).degree = s.sup fun i => (f i).degree

Defined in

Mathlib.Algebra.Polynomial.BigOperators

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra