mul_comm_of_commute

Mathlib.Algebra.Algebra.Operations

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

English

If every element of M commutes with every element of N, then M * N = N * M.

Русский

Если каждый элемент M коммутирует с каждым элементом N, то M * N = N * M.

LaTeX

$$$ (\forall m \in M, \forall n \in N, \, Commute\; m\, n) \Rightarrow M * N = N * M $$$

Lean4

theorem mul_comm_of_commute (h : ∀ m ∈ M, ∀ n ∈ N, Commute m n) : M * N = N * M :=
  toAddSubmonoid_injective <| AddSubmonoid.mul_comm_of_commute h

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

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

Разделы

Аффилиация

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