inv_inl — Mathlib

English

In a division semiring context, the inverse of inl(r) is inl(r^{-1}).

Русский

В контексте делимого полупрямого кольца обратный элемент inl(r) равен inl(r^{-1}).

LaTeX

$$$ (inl(r))^{-1} = inl(r^{-1}) $$$

Lean4

protected theorem inv_inl (r : R) : (inl r)⁻¹ = (inl (r⁻¹ : R) : tsze R M) :=
  by
  ext
  · rw [fst_inv, fst_inl, fst_inl]
  · rw [snd_inv, fst_inl, snd_inl, snd_inl, smul_zero, smul_zero, neg_zero]

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