mem_coeSubmodule — Mathlib

English

Membership in coSubmodule I corresponds to the existence of a witness from I mapping to x under the algebra map.

Русский

Членство в coSubmodule I эквивалентно существованию x' ∈ I such that algebraMap x' = algebraMap x.

LaTeX

$$x ∈ IsLocalization.coeSubmodule P I \iff \exists x' ∈ I, algebraMap R P x' = algebraMap R P x$$

Lean4

@[simp] -- Ensure `simp` is confluent for `x ∈ ((I : Ideal R) : FractionalIdeal S P)`.

theorem mem_coeSubmodule {x : P} {I : Ideal R} : x ∈ coeSubmodule P I ↔ ∃ x', x' ∈ I ∧ algebraMap R P x' = x :=
  Iff.rfl

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