add — Mathlib

English

The sum of two polynomials homogeneous of the same degree n is homogeneous of degree n.

Русский

Сумма двух полиномов, однородных по степени n, однородна по степени n.

LaTeX

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

Lean4

theorem add (hφ : IsHomogeneous φ n) (hψ : IsHomogeneous ψ n) : IsHomogeneous (φ + ψ) n :=
  (homogeneousSubmodule σ R n).add_mem hφ hψ

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