English
There is a canonical way to view a nonzero integral ideal as an invertible fractional ideal, given by mk0.
Русский
Существует канонический способ рассмотреть ненулевой интегральный идеал как обратимый дробный идеал — mk0.
LaTeX
$$$\text{mk0} : (\mathrm{Ideal}(R))^{0} \to \mathrm{Units}(\mathrm{FractionalIdeal}(\mathrm{nonZeroDivisors}R, K)).$$$
Lean4
/-- Send a nonzero integral ideal to an invertible fractional ideal. -/
noncomputable def mk0 [IsDedekindDomain R] : (Ideal R)⁰ →* (FractionalIdeal R⁰ K)ˣ
where
toFun I := Units.mk0 I (coeIdeal_ne_zero.mpr <| mem_nonZeroDivisors_iff_ne_zero.mp I.2)
map_one' := by simp
map_mul' x y := by simp
