eq_iff_exists — Mathlib

English

Two base-algebra images are equal if and only if there exists a multiplier in M that equates the products.

Русский

Два образа из R в S равны тогда и только тогда, когда существует множитель в M, приводящий равенство продуктов.

LaTeX

$$$\\alpha = \\beta \\iff \\exists c \\in M, c x = c y$ для соответствующих x,y$$

Lean4

@[inherit_doc IsLocalization.exists_of_eq]
theorem eq_iff_exists {x y} : algebraMap R S x = algebraMap R S y ↔ ∃ c : M, ↑c * x = ↑c * y :=
  Iff.intro IsLocalization.exists_of_eq fun ⟨c, h⟩ ↦
    by
    apply_fun algebraMap R S at h
    rw [map_mul, map_mul] at h
    exact (IsLocalization.map_units S c).mul_right_inj.mp h

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