ringInverse_ringInverse — Mathlib

English

If a and b commute, then their ring inverses commute: Ring.inverse(a) and Ring.inverse(b) commute.

Русский

Если a и b коммутируют, то их обратные по кольцу также коммутируют.

LaTeX

$$$Commute( Ring.inverse(a), Ring.inverse(b) ) \text{ if } Commute(a,b)$$$

Lean4

theorem ringInverse_ringInverse {a b : M₀} (h : Commute a b) : Commute (Ring.inverse a) (Ring.inverse b) :=
  (Ring.mul_inverse_rev' h.symm).symm.trans <| (congr_arg _ h.symm.eq).trans <| Ring.mul_inverse_rev' h

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