English
The fractional ideals of a domain R are R-submodules of a localization P that become contained in R after multiplying by some nonzero a in R.
Русский
Дробные идеалы области R — это R-подмодули локализации P, которые после умножения на некоторое ненулевое a из R подмножество R.
LaTeX
$$$\\text{FractionalIdeal}(S,P) := \\{ I \\subseteq P \\mid I \\text{ is an } R\\text{-submodule of } P \\text{ with } \\exists a\\in S, aI\\subseteq R \\}$$$
Lean4
/-- The fractional ideals of a domain `R` are ideals of `R` divided by some `a ∈ R`.
More precisely, let `P` be a localization of `R` at some submonoid `S`,
then a fractional ideal `I ⊆ P` is an `R`-submodule of `P`,
such that there is a nonzero `a : R` with `a I ⊆ R`.
-/
def FractionalIdeal :=
{ I : Submodule R P // IsFractional S I }
