one_mul

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.one_mul

English

Re-statement: 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

protected theorem one_mul : (1 : Submodule R A) * M = M :=
  Submodule.one_smul _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru