English
Under a localization with h: S ≤ nonZeroDivisors R, x ∈ I iff there exists x′ ∈ I with algebraMap x′ = algebraMap x.
Русский
При локализации с h: S ≤ nonZeroDivisors R, x ∈ I тогда существует x′ ∈ I такое, что algebraMap x′ = algebraMap x.
LaTeX
$$$(\exists x', x' \in I \land algebraMap R P x' = algebraMap R P x) \iff x \in I$$
Lean4
/-- Map an ideal `I` to a fractional ideal by forgetting `I` is integral.
This is the function that implements the coercion `Ideal R → FractionalIdeal S P`. -/
@[coe]
def coeIdeal (I : Ideal R) : FractionalIdeal S P :=
⟨coeSubmodule P I, isFractional_of_le_one _ <| by simpa using coeSubmodule_mono P (le_top : I ≤ ⊤)⟩
-- Is a `CoeTC` rather than `Coe` to speed up failing inference, see library note [use has_coe_t]
