inv_mem_centralizer₀ — Mathlib

English

In a group with zero, if a ∈ centralizer s, then a^{-1} ∈ centralizer s; centralizer is closed under inversion.

Русский

В группе с нулём, если a ∈ centralizer s, то a^{-1} ∈ centralizer s; центральизатор замкнут по инверсии.

LaTeX

$$$a \in centralizer(s) \Rightarrow a^{-1} \in centralizer(s)$$$

Lean4

@[simp]
theorem inv_mem_centralizer₀ (ha : a ∈ centralizer s) : a⁻¹ ∈ centralizer s :=
  by
  obtain rfl | ha₀ := eq_or_ne a 0
  · rw [inv_zero]
    exact zero_mem_centralizer
  · rintro c hc
    rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]

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