Theorems · Theorem · field theory

Polynomial.card_support_eq

∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R} {n : ℕ},
  f.support.card = n ↔
    ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, Polynomial.C (x i) * Polynomial.X ^ k i

Defined in

Mathlib.Algebra.Polynomial.EraseLead

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring