inv_right₀ — Mathlib

English

In a group with zero, if h: SemiconjBy a x y then SemiconjBy a x⁻¹ y⁻¹ under suitable conditions.

Русский

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

LaTeX

$$$h: SemiconjBy\ a\ x\ y \Rightarrow SemiconjBy\ a\ x^{-1}\ y^{-1}$$$

Lean4

theorem inv_right₀ (h : SemiconjBy a x y) : SemiconjBy a x⁻¹ y⁻¹ :=
  by
  by_cases ha : a = 0
  · simp only [ha, zero_left]
  by_cases hx : x = 0
  · subst x
    simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
    simp [h.resolve_right ha]
  · have := mul_ne_zero ha hx
    rw [h.eq, mul_ne_zero_iff] at this
    exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h

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