associatesNonZeroDivisorsEquivIsPrincipal_mul

English

The principal-equivalence is a monoid hom: the image of a product equals the product of the images.

Русский

Главное эквивалентное отображение сохраняет произведение: образ произведения равен произведению образов.

LaTeX

$$$(associatesNonZeroDivisorsEquivIsPrincipal\ R (x * y) : Ideal R) = (associatesNonZeroDivisorsEquivIsPrincipal\ R x) * (associatesNonZeroDivisorsEquivIsPrincipal\ R y)$$$

Lean4

theorem associatesNonZeroDivisorsEquivIsPrincipal_mul (x y : Associates R⁰) :
    (associatesNonZeroDivisorsEquivIsPrincipal R (x * y) : Ideal R) =
      (associatesNonZeroDivisorsEquivIsPrincipal R x) * (associatesNonZeroDivisorsEquivIsPrincipal R y) :=
  by simp_rw [associatesNonZeroDivisorsEquivIsPrincipal_coe, map_mul, Submonoid.coe_mul, associatesEquivIsPrincipal_mul]

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