units_inv_mem_center — Mathlib

English

If a unit a lies in the center of M, then its inverse a^{-1} also lies in the center of M.

Русский

Если элемент-единица a лежит в центре M, то и его обратное a^{-1} лежит в центре M.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem units_inv_mem_center {a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M :=
  by
  rw [Semigroup.mem_center_iff] at *
  exact (Commute.units_inv_right <| ha ·)

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