eq — Mathlib · SciLib

English

Let a1, b1 be elements of R and a2, b2 be elements of M. Then the fractions a1/a2 and b1/b2 are equal in the localization if and only if there exists c in M such that c·(b2·a1) = c·(a2·b1) in R.

Русский

Пусть a1, b1 ∈ R и a2, b2 ∈ M. Тогда дроби a1/a2 и b1/b2 равны в локализации тогда и только тогда, когда существует c ∈ M такое, что c·(b2·a1) = c·(a2·b1) в R.

LaTeX

$$$\\dfrac{a_1}{a_2} = \\dfrac{b_1}{b_2} \\iff \\exists c \\in M,\; c\\,(b_2 a_1) = c\\,(a_2 b_1).$$$

Lean4

protected theorem eq {a₁ b₁} {a₂ b₂ : M} : mk' S a₁ a₂ = mk' S b₁ b₂ ↔ ∃ c : M, ↑c * (↑b₂ * a₁) = c * (a₂ * b₁) :=
  (toLocalizationMap M S).eq

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