eq_iff_eq — Mathlib

English

For x1, x2 ∈ R and y1, y2 ∈ M, the equalities mk' S x1 y1 = mk' S x2 y2 and mk' P x1 y1 = mk' P x2 y2 are equivalent.

Русский

Для x1,x2 ∈ R и y1,y2 ∈ M равенства mk' S x1 y1 = mk' S x2 y2 и mk' P x1 y1 = mk' P x2 y2 взаимно эквивалентны.

LaTeX

$$$mk' S x_1 y_1 = mk' S x_2 y_2 \\iff mk' P x_1 y_1 = mk' P x_2 y_2$$$

Lean4

theorem eq_iff_eq [Algebra R P] [IsLocalization M P] {x y} :
    algebraMap R S x = algebraMap R S y ↔ algebraMap R P x = algebraMap R P y :=
  (toLocalizationMap M S).eq_iff_eq (toLocalizationMap M P)

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