mk'_eq_iff_mk'_eq — Mathlib

English

If in R we have a2⋅b1 = b2⋅a1 with a1,a2 ∈ R and b1,b2 ∈ M, then mk' S a1 a2 = mk' S b1 b2.

Русский

Пусть a1,a2 ∈ R и b1,b2 ∈ M такие, что a2 b1 = b2 a1; тогда mk' S a1 a2 = mk' S b1 b2.

LaTeX

$$$\\text{If } \\uparrow a_2 \\cdot b_1 = \\uparrow b_2 \\cdot a_1, \\text{ then } mk' S a_1 a_2 = mk' S b_1 b_2.$$$

Lean4

theorem mk'_eq_iff_mk'_eq [Algebra R P] [IsLocalization M P] {x₁ x₂} {y₁ y₂ : M} :
    mk' S x₁ y₁ = mk' S x₂ y₂ ↔ mk' P x₁ y₁ = mk' P x₂ y₂ :=
  (toLocalizationMap M S).mk'_eq_iff_mk'_eq (toLocalizationMap M P)

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