mul_inv_mem_iff — Mathlib

English

In a group G with star, a · b^{-1} is unitary iff star(a) · a = star(b) · b.

Русский

В группе G со звездой элемент a b^{-1} единичен тогда и только тогда, когда star(a) a = star(b) b.

LaTeX

$$$ a b^{-1} \in \mathrm{unitary}(G) \iff \star a \cdot a = \star b \cdot b $$$

Lean4

theorem mul_inv_mem_iff {G : Type*} [Group G] [StarMul G] (a b : G) : a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b :=
  by
  rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc, inv_mul_eq_iff_eq_mul, mul_one, ←
    mul_assoc, mul_inv_eq_iff_eq_mul]

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