associated_unit_mul_left_iff — Mathlib

English

Let N be a monoid. If u is a unit, then (↑u * a) is associated with b iff a is associated with b; i.e., multiplication by a unit on the left commutes with the association relation.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem associated_unit_mul_left_iff {N : Type*} [CommMonoid N] {a b : N} {u : Units N} :
    Associated (↑u * a) b ↔ Associated a b :=
  associated_isUnit_mul_left_iff u.isUnit

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