map_mk' — Mathlib

English

The map sends mk'(S, x, y) to mk'(Q, g x, (g y, hy y.2)); i.e., fractions map to the corresponding fractions in Q.

Русский

Отображение отправляет mk'(S, x, y) в mk'(Q, g x, ⟨g y, hy y.2⟩); дроби переходят в соответствующие дроби в Q.

LaTeX

$$$ map\\ Q\\ g\\ hy\\ (mk'\\ S\\ x\\ y) = mk'\\ Q\\ (g\\ x)\\ ⟨g\\ y, hy y.2⟩. $$$

Lean4

theorem map_mk' (x) (y : M) : map Q g hy (mk' S x y) = mk' Q (g x) ⟨g y, hy y.2⟩ :=
  Submonoid.LocalizationMap.map_mk' (toLocalizationMap M S) (g := g.toMonoidHom) (fun y => hy y.2) (k :=
    toLocalizationMap T Q) ..

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