lift_eq_iff — Mathlib

English

Two elements (x1,y1) and (x2,y2) in R×M have equal lifts if and only if g(x1 y2) = g(x2 y1).

Русский

Две дроби (x1/y1) и (x2/y2) имеют одинаковые образы под lift тогда и только тогда, когда g(x1 y2) = g(x2 y1).

LaTeX

$$$ \\mathrm{lift}\\;hg (mk'\\ S\\ x_1\\ y_1) = \\mathrm{lift}\\;hg (mk'\\ S\\ x_2\\ y_2) \\;\\Longleftrightarrow\\; g(x_1 y_2) = g(x_2 y_1). $$$

Lean4

theorem lift_eq_iff {x y : R × M} : lift hg (mk' S x.1 x.2) = lift hg (mk' S y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2) :=
  (toLocalizationMap M S).lift_eq_iff _

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