mul — Mathlib

English

The product of homogeneous polynomials of degrees m and n is homogeneous of degree m + n.

Русский

Произведение однородных по степеням m и n полиномов однородно по степени m + n.

LaTeX

$$(IsHomogeneous(\phi, m) \land IsHomogeneous(\psi, n)) \Rightarrow IsHomogeneous(\phi * \psi, m + n)$$

Lean4

theorem mul (hφ : IsHomogeneous φ m) (hψ : IsHomogeneous ψ n) : IsHomogeneous (φ * ψ) (m + n) :=
  homogeneousSubmodule_mul m n <| Submodule.mul_mem_mul hφ hψ

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