Theorems · Theorem · algebraic geometry

Polynomial.eval_homogenize

∀ {K : Type u_1} [inst : Semifield K] {p : Polynomial K} {n : ℕ},
  p.natDegree ≤ n →
    ∀ (x : Fin 2 → K), x 1 ≠ 0 → (MvPolynomial.eval x) (p.homogenize n) = Polynomial.eval (x 0 / x 1) p * x 1 ^ n

Defined in

Mathlib.Algebra.Polynomial.Homogenize

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semifield