mul_mem_mul_rev — Mathlib

English

If m∈M and n∈N then n*m ∈ M*N; equivalently, multiplying in the opposite order still lands in the product submodule.

Русский

Если m∈M и n∈N, то n*m ∈ M*N; умножение в обратном порядке сохраняет принадлежность произведению подмодулей.

LaTeX

$$$\forall m \in M, \forall n \in N,\; n \cdot m \in M \cdot N$$$

Lean4

theorem mul_mem_mul_rev (hm : m ∈ M) (hn : n ∈ N) : n * m ∈ M * N :=
  mul_comm m n ▸ mul_mem_mul hm hn

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