Theorems · Theorem · algebraic geometry

Polynomial.coeff_homogenize

∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ) (m : Fin 2 →₀ ℕ),
  MvPolynomial.coeff m (p.homogenize n) = if m 0 + m 1 = n then p.coeff (m 0) else 0

Defined in

Mathlib.Algebra.Polynomial.Homogenize

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiring