Theorems · Theorem · field theory

Polynomial.support_trinomial

∀ {R : Type u} [inst : Semiring R] {k m n : ℕ},
  k < m →
    m < n →
      ∀ {x y z : R},
        x ≠ 0 →
          y ≠ 0 →
            z ≠ 0 →
              (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.Coeff

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring