r_of_eq — Mathlib

English

If x=(x1,x2) and y=(y1,y2) are in M×S and the cross-multiplication equality y2·x1 = x2·y1 holds, then x and y are related in Localization(S).

Русский

Пусть x=(x1,x2), y=(y1,y2) лежат в M×S и выполнено y2·x1 = x2·y1; тогда x и y связаны в Localization(S).

LaTeX

$$$\\forall x=(x_1,x_2), y=(y_1,y_2) \\in M \\times S,\\ (y_2 x_1 = x_2 y_1) \\Rightarrow r_S x y.$$$

Lean4

@[to_additive]
theorem r_of_eq {x y : M × S} (h : ↑y.2 * x.1 = ↑x.2 * y.1) : r S x y :=
  r_iff_exists.2 ⟨1, by rw [h]⟩

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