mul_le — Mathlib

English

Multiplication of submodules respects inclusion: M * N ≤ P iff ∀ m ∈ M, ∀ n ∈ N, m n ∈ P.

Русский

Умножение подмодулов сохраняет включение: M * N ≤ P тогда и только тогда, когда для всех m ∈ M, n ∈ N выполняется m n ∈ P.

LaTeX

$$$ M * N \le P \iff \forall m \in M, \forall n \in N, m n \in P $$$

Lean4

theorem mul_le : M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P :=
  smul_le

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