Theorems · Theorem · field theory

Polynomial.card_support_binomial

∀ {R : Type u} [inst : Semiring R] {k m : ℕ},
  k ≠ m →
    ∀ {x y : R},
      x ≠ 0 → y ≠ 0 → (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support.card = 2

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