one_mem_center — Mathlib

English

In a multiplicative group with unit, the unit element 1 lies in the center of M.

Русский

В мультипликативной группе с единицей 1 лежит в центре M.

LaTeX

$$$ 1 \in \mathrm{center}(M) $$$

Lean4

@[to_additive (attr := simp) zero_mem_addCenter]
theorem one_mem_center : (1 : M) ∈ Set.center M
    where
  comm _ := by rw [commute_iff_eq, one_mul, mul_one]
  left_assoc _ _ := by rw [one_mul, one_mul]
  right_assoc _ _ := by rw [mul_one, mul_one]

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