homogenize_mul — Mathlib

English

For p,q ∈ R[X], if natDegree p ≤ m and natDegree q ≤ n, then homogenize(p q)(m+n) = homogenize p m · homogenize q n.

Русский

Пусть p,q ∈ R[X], deg(p) ≤ m и deg(q) ≤ n. Тогда homogenize(p q)(m+n) = homogenize p m · homogenize q n.

LaTeX

$$$\\operatorname{homogenize}(p q, m+n) = \\operatorname{homogenize}(p, m) \\cdot \\operatorname{homogenize}(q, n).$$$

Lean4

theorem homogenize_mul (p q : R[X]) {m n : ℕ} (hm : natDegree p ≤ m) (hn : natDegree q ≤ n) :
    homogenize (p * q) (m + n) = homogenize p m * homogenize q n :=
  by
  apply homogenize_eq_of_isHomogeneous
  · apply_rules [MvPolynomial.IsHomogeneous.mul, isHomogeneous_homogenize]
  · simp [*]

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