associatesNonZeroDivisorsEquivIsPrincipal_map_one

English

The image of 1 under the principal-equivalence is the unit ideal 1.

Русский

Образ единицы при главном эквиваленте равен единице как идеалу.

LaTeX

$$$(associatesNonZeroDivisorsEquivIsPrincipal\ R\ 1 : \mathrm{Ideal} R) = 1$$$

Lean4

@[simp]
theorem associatesNonZeroDivisorsEquivIsPrincipal_map_one :
    (associatesNonZeroDivisorsEquivIsPrincipal R 1 : Ideal R) = 1 := by
  rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_one, OneMemClass.coe_one, associatesEquivIsPrincipal_map_one]

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