invertible_mk'_one — Mathlib

English

For every s ∈ M, the element mk' S (1 : R) s is invertible in S, with inverse given by algebraMap R S s.

Русский

Для каждого s ∈ M элемент mk' S (1 : R) s обратим в S, обратное равно algebraMap_R^S(s).

LaTeX

$$$\\text{Invertible} (mk' S (1 : R) s)$ with inverse $\\text{algebraMap } R S s$$$

Lean4

@[simps]
noncomputable instance invertible_mk'_one (s : M) : Invertible (IsLocalization.mk' S (1 : R) s)
    where
  invOf := algebraMap R S s
  invOf_mul_self := by simp
  mul_invOf_self := by simp

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