Theorems · Theorem · algebraic geometry

Polynomial.homogenize_monomial

∀ {R : Type u_1} [inst : CommSemiring R] {m n : ℕ},
  m ≤ n → ∀ (r : R), ((Polynomial.monomial m) r).homogenize n = (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

Defined in

Mathlib.Algebra.Polynomial.Homogenize

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiring