mul_mem_mul — Mathlib

English

The additive submonoid underlying M * N equals the product of the additive submonoids underlying M and N: (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid.

Русский

Аддитивная подмономоида подмодуля произведения совпадает с произведением аддитивных подмономоидов: (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid.

LaTeX

$$$ (M * N)^{+} = M^{+} * N^{+} $$$

Lean4

theorem mul_mem_mul (hm : m ∈ M) (hn : n ∈ N) : m * n ∈ M * N :=
  smul_mem_smul hm hn

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