inv_mem_center — Mathlib

English

Let M be a division monoid and a be an element of the center of M. Then the inverse a^{-1} also lies in the center of M; i.e., a^{-1} commutes with every element of M.

Русский

Пусть M — делимый моноид и a принадлежит центру M. Тогда обратный к a, a^{-1}, также лежит в центре M; то есть он коммутирует с любым элементом M.

LaTeX

$$$ a \\in Z(M) \\Rightarrow a^{-1} \\in Z(M) $$$

Lean4

@[to_additive (attr := simp) neg_mem_addCenter]
theorem inv_mem_center (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M :=
  by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← inv_inj, mul_inv_rev, inv_inv, ha.comm, mul_inv_rev, inv_inv]

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