Theorems · Theorem · field theory

Polynomial.card_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.card =
                3

Defined in

Mathlib.Algebra.Polynomial.Coeff

Cited by

2 results in Mathlib

Foundations

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

Assumes

Semiring