mul — Mathlib

English

If a ∈ A(i) and b ∈ A(j) are homogeneous, then their product a b is homogeneous of degree i + j.

Русский

Если a ∈ A(i) и b ∈ A(j) — однородные элементы, то произведение a b однородно степени i + j.

LaTeX

$$$ a \in A(i) \wedge b \in A(j) \Rightarrow ab \in A(i+j) $$$

Lean4

theorem mul [Add ι] [Mul R] {A : ι → S} [SetLike.GradedMul A] {a b : R} :
    SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem A b → SetLike.IsHomogeneousElem A (a * b)
  | ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i + j, SetLike.mul_mem_graded hi hj⟩

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