associated_mul_unit_right_iff — Mathlib

English

Let N be a monoid. If u is a unit, then a is associated with (b*u) iff a is associated with b; i.e., right multiplication by a unit preserves associativity even when the unit is represented as a Units element.

Русский

Пусть N — моноид. Если u — единица, то a ассоциировано с (b·u) тогда и только тогда, когда a ассоциировано с b.

LaTeX

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

Lean4

@[simp]
theorem associated_mul_unit_right_iff {N : Type*} [Monoid N] {a b : N} {u : Units N} :
    Associated a (b * u) ↔ Associated a b :=
  associated_mul_isUnit_right_iff u.isUnit

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