associatesEquivIsPrincipal_mul — Mathlib

English

The equivalence respects multiplication: the image of a product of associates corresponds to the product of the images of the factors.

Русский

Эквивалентность сохраняет умножение: образ произведения ассоциантов равен произведению образов факторов.

LaTeX

$$$associatesEquivIsPrincipal(R)(x\cdot y) = (associatesEquivIsPrincipal(R)x) \cdot (associatesEquivIsPrincipal(R)y)$$$

Lean4

theorem associatesEquivIsPrincipal_mul (x y : Associates R) :
    (associatesEquivIsPrincipal R (x * y) : Ideal R) =
      (associatesEquivIsPrincipal R x) * (associatesEquivIsPrincipal R y) :=
  by
  rw [← quot_out x, ← quot_out y]
  simp_rw [mk_mul_mk, associatesEquivIsPrincipal_apply, span_singleton_mul_span_singleton]

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