associatesNonZeroDivisorsEquivIsPrincipal_coe

English

The two canonical identifications are compatible with each other on coefficients: the principal-ideals image agrees with the image under the standard associates-equivalences.

Русский

Две канонические идентификации совместимы друг с другом на коэффициентах: образ при главном эквиваленте совпадает с образом при стандартных эквивалентностях ассоциатов.

LaTeX

$$$(associatesNonZeroDivisorsEquivIsPrincipal\ R\ x) = (associatesEquivIsPrincipal\ R\ (associatesNonZeroDivisorsEquiv.symm\ x))$$$

Lean4

theorem associatesNonZeroDivisorsEquivIsPrincipal_coe (x : Associates R⁰) :
    (associatesNonZeroDivisorsEquivIsPrincipal R x : Ideal R) =
      (associatesEquivIsPrincipal R (associatesNonZeroDivisorsEquiv.symm x)) :=
  rfl

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