English
Let R be a commutative domain. There exists a natural multiplicative equivalence between the monoid of associates of R and the submonoid of principal ideals of R; more precisely, the map sends the class of x to the principal ideal (x).
Русский
Пусть R — коммутативное доменное кольцо. Существует естественный минимальный по умножению эквивалент между моноидом ассоциатов R и подмоноидом главных идеалов R; точнее, отображение отправляет классу x в порожденный этим элементом главный идеал (x).
LaTeX
$$$\mathrm{Associates}(R) \xrightarrow{\simeq_*} \mathrm{isPrincipalSubmonoid}(R)$$$
Lean4
/-- The `MulEquiv` version of `Ideal.associatesEquivIsPrincipal`. -/
noncomputable def associatesMulEquivIsPrincipal : Associates R ≃* isPrincipalSubmonoid R
where
__ := associatesEquivIsPrincipal R
map_mul' _
_ :=
by
rw [Subtype.ext_iff]
-- This `erw` is needed to see through `{I // IsPrincipal I} = ↑(isPrincipalSubmonoid R)`:
-- we can redefine `associatesEquivIsPrincipal` to get rid of this `erw` but then we'd need
-- to add one in `associatesNonZeroDivisorsEquivIsPrincipal`.
erw [associatesEquivIsPrincipal_mul]
rfl
