Theorems · Theorem · field theory

Polynomial.support_trinomial_subset

∀ {R : Type u} [inst : Semiring R] (k m n : ℕ) (x y z : R),
  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆
    {k, m, n}

Defined in

Mathlib.Algebra.Polynomial.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

Semiring