invOf_left — Mathlib

English

Let α be a monoid and a, b ∈ α with b invertible. If b commutes with a, then b^{-1} commutes with a.

Русский

Пусть α — моноид и a, b ∈ α, где b обратим. Если b коммутирует с a, то b^{-1} коммутирует с a.

LaTeX

$$$b^{-1} a = a b^{-1}$$$

Lean4

theorem invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b a) : Commute (⅟b) a :=
  calc
    ⅟b * a = ⅟b * (a * b * ⅟b) := by simp [mul_assoc]
    _ = ⅟b * (b * a * ⅟b) := by rw [h.eq]
    _ = a * ⅟b := by simp [mul_assoc]

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