English
There is a coercion from ideals to fractional ideals given by coeIdeal, interpreting I ↦ coeIdeal I.
Русский
Существуют преобразование из идеалов в дробные идеалы, задаваемое коэффициентом coeIdeal, которое отправляет I в coeIdeal I.
LaTeX
$$$coeIdeal : \mathrm{Ideal}\ R \to \mathrm{FractionalIdeal}\ S\ P$$$
Lean4
/-- Map an ideal `I` to a fractional ideal by forgetting `I` is integral.
This is a bundled version of `IsLocalization.coeSubmodule : Ideal R → Submodule R P`,
which is not to be confused with the `coe : FractionalIdeal S P → Submodule R P`,
also called `coeToSubmodule` in theorem names.
This map is available as a ring hom, called `FractionalIdeal.coeIdealHom`.
-/
instance : CoeTC (Ideal R) (FractionalIdeal S P) :=
⟨fun I => coeIdeal I⟩
