homogenize_C — Mathlib

English

For any c in R and any n, homogenize of the constant polynomial C c equals C c times X_1^n.

Русский

Для каждого c ∈ R и любого n гомогенизация константного многочлена C c равна C c умножить на X_1^n.

LaTeX

$$$\\operatorname{homogenize}(\\mathsf{C}(c), n) = \\mathsf{C}(c) \\cdot X_1^{n}.$$$

Lean4

@[simp]
theorem homogenize_C (c : R) (n : ℕ) : homogenize (.C c) n = .C c * .X 1 ^ n := by
  simpa [MvPolynomial.C_mul_X_pow_eq_monomial] using homogenize_monomial (Nat.zero_le n) c

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