associated_mul_isUnit_right_iff — Mathlib

English

Let N be a monoid and u a unit. Then for all a, b in N, a is associated with (b*u) iff a is associated with b; i.e., right-multiplying by a unit preserves associativity.

Русский

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

LaTeX

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

Lean4

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

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