mul_comm_of_commute — Mathlib

English

If every pair m ∈ M, n ∈ N commute, then M * N = N * M.

Русский

Если для каждого m ∈ M и n ∈ N выполняется, что m и n commute, то 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 :=
  le_antisymm (mul_le.mpr fun m hm n hn ↦ h m hm n hn ▸ mul_mem_mul hn hm)
    (mul_le.mpr fun n hn m hm ↦ h m hm n hn ▸ mul_mem_mul hm hn)

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