associated_unit_mul_right_iff — Mathlib

English

Let N be a commutative monoid. If u is a unit, then (↑u * b) is associated with a iff b is associated with a; i.e., left-multiplication by a unit on the left (as Units) preserves associativity.

Русский

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

LaTeX

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

Lean4

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

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