lift_mk'_spec — Mathlib

English

For g: R → P, hg: ∀ y ∈ M, IsUnit(g(y)), and x ∈ R, y ∈ M, the equality lift hg (mk'(S, x, y)) = g(x) · (g(y))^{-1} holds by definition.

Русский

Для g: R → P, hg: ∀ y ∈ M, IsUnit(g(y)), и x ∈ R, y ∈ M, равенство lift hg (mk'(S, x, y)) выражается как g(x) · (g(y))^{-1} по определению.

LaTeX

$$$ lift\\ hg (mk'\\ S\\ x\\ y) = g(x) \\cdot (g(y))^{-1}. $$$

Lean4

theorem lift_mk'_spec (x v) (y : M) : lift hg (mk' S x y) = v ↔ g x = g y * v :=
  (toLocalizationMap M S).lift_mk'_spec _ _ _ _

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