inv_symm_left_iff₀ — Mathlib

English

In a group with zero, if h is SemiconjBy a x y, then SemiconjBy a⁻¹ y x.

Русский

В группе с нулём, если h: SemiconjBy a x y, то SemiconjBy a⁻¹ y x.

LaTeX

$$$\text{If } h:\ SemiconjBy\ a\ x\ y, \text{ then } SemiconjBy\ a^{-1}\ y\ x$$$

Lean4

@[simp]
theorem inv_symm_left_iff₀ : SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x :=
  Classical.by_cases (fun ha : a = 0 => by simp only [ha, inv_zero, SemiconjBy.zero_left]) fun ha =>
    @units_inv_symm_left_iff _ _ (Units.mk0 a ha) _ _

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