mem_localizationLocalizationSubmodule

English

A criterion: x ∈ localizationLocalizationSubmodule M N iff there exist y ∈ N and z ∈ M such that algebraMap_R_S x = y · algebraMap_R_S z.

Русский

Критерий членства: x ∈ localizationLocalizationSubmodule M N тогда и только тогда, когда существует y ∈ N и z ∈ M с algebraMap_R_S x = y · algebraMap_R_S z.

LaTeX

$$$x \in localizationLocalizationSubmodule M N \iff \exists y\in N, \exists z\in M, \mathrm{algebraMap}_{R S}(x) = y \cdot \mathrm{algebraMap}_{R S}(z)$$$

Lean4

@[simp]
theorem mem_localizationLocalizationSubmodule {x : R} :
    x ∈ localizationLocalizationSubmodule M N ↔ ∃ (y : N) (z : M), algebraMap R S x = y * algebraMap R S z :=
  by
  rw [localizationLocalizationSubmodule, Submonoid.mem_comap, Submonoid.mem_sup]
  constructor
  · rintro ⟨y, hy, _, ⟨z, hz, rfl⟩, e⟩
    exact ⟨⟨y, hy⟩, ⟨z, hz⟩, e.symm⟩
  · rintro ⟨y, z, e⟩
    exact ⟨y, y.prop, _, ⟨z, z.prop, rfl⟩, e.symm⟩

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