homogenize_X_pow — Mathlib

English

Let R be a commutative semiring. For natural numbers m and n with m ≤ n, the homogenization of the monomial X^m in R[X] to degree n equals X_0^m X_1^{n−m}.

Русский

Пусть R — коммутативная полукольцо. Пусть m,n ∈ ℕ и m ≤ n. Гомогенизация монома X^m по степени n в R[X] равна X_0^m X_1^{n−m}.

LaTeX

$$$\\operatorname{homogenize}(X^m, n) = X_0^m \\cdot X_1^{\\,n-m} \\quad (m \\le n).$$$

Lean4

@[simp]
theorem homogenize_X_pow {m n : ℕ} (h : m ≤ n) : homogenize (X ^ m : R[X]) n = .X 0 ^ m * .X 1 ^ (n - m) := by
  rw [X_pow_eq_monomial, homogenize_monomial h, Finsupp.update_eq_add_single (by simp),
    MvPolynomial.monomial_single_add, ← MvPolynomial.X_pow_eq_monomial]

Похожие утверждения