associated_isUnit_mul_right_iff — Mathlib

English

Let N be a commutative monoid and u a unit. Then for all a, b in N, a is associated with (u*b) iff a is associated with b; i.e., left-multiplying by a unit does not change associativity in a commutative setting.

Русский

Пусть N — коммутативный моноид и u — единица. Тогда для любых a, b ∈ N верно: a ассоциировано с (u·b) ⇔ a ассоциировано с b.

LaTeX

$$$ [CommMonoid N] {a b u : N} (hu : IsUnit u) : Associated a (u * b) \leftrightarrow Associated a b $$$

Lean4

theorem associated_isUnit_mul_right_iff {N : Type*} [CommMonoid N] {a u b : N} (hu : IsUnit u) :
    Associated a (u * b) ↔ Associated a b :=
  Associated.comm.trans <| (associated_isUnit_mul_left_iff hu).trans Associated.comm

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