associatesNonZeroDivisorsMulEquivIsPrincipal

English

There is a multiplicative equivalence between the associates of nonzero divisors and the principal-nonzero-divisors submonoid.

Русский

Существует мультипликативное эквивалентное отображение между ассоциатами не нулевых делителей и подмоноидом главных не нулевых делителей.

LaTeX

$$$\mathrm{associatesNonZeroDivisorsMulEquivIsPrincipal} : \mathrm{Associates}(R)^{0} \cong_*(\text{isPrincipalNonZeroDivisorsSubmonoid } R)$$$

Lean4

/-- The `MulEquiv` version of `Ideal.associatesNonZeroDivisorsEquivIsPrincipal`. -/
noncomputable def associatesNonZeroDivisorsMulEquivIsPrincipal :
    Associates R⁰ ≃* (isPrincipalNonZeroDivisorsSubmonoid R)
    where
  __ := associatesNonZeroDivisorsEquivIsPrincipal R
  map_mul' _
    _ :=
    by
    rw [Subtype.ext_iff, Subtype.ext_iff, Equiv.toFun_as_coe, associatesNonZeroDivisorsEquivIsPrincipal_mul]
    rfl

Похожие утверждения