sub — Mathlib

English

The difference of two homogeneous polynomials 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 sub (hφ : IsHomogeneous φ n) (hψ : IsHomogeneous ψ n) : IsHomogeneous (φ - ψ) n :=
  (homogeneousSubmodule σ R n).sub_mem hφ hψ

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