Theorems · Theorem · field theory

Polynomial.card_support_eq_three

∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R},
  f.support.card = 3 ↔
    ∃ k m n,
      ∃ (_ : k < m) (_ : m < n),
        ∃ x y z,
          ∃ (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
            f =
              Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n

Defined in

Mathlib.Algebra.Polynomial.EraseLead

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring