zero_mem_center — Mathlib

English

In any multiplicative structure with zero, the zero element commutes with every other element: 0 · x = x · 0 for all x.

Русский

В любой структуре с умножением и нулём ноль коммутирует с каждым элементом: 0·x = x·0 для всех x.

LaTeX

$$$\forall x,\ 0\cdot x = x\cdot 0$$$

Lean4

@[simp]
theorem zero_mem_center : (0 : M₀) ∈ center M₀
    where
  comm _ := by rw [commute_iff_eq, zero_mul, mul_zero]
  left_assoc _ _ := by rw [zero_mul, zero_mul, zero_mul]
  right_assoc _ _ := by rw [mul_zero, mul_zero, mul_zero]

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