associated_mul_unit_left_iff — Mathlib

English

Let N be a monoid and a, b in N with u a unit. Then (a*u) is associated with b iff a is associated with b; i.e., left-multiplication by a unit on the left preserves associativity.

Русский

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

LaTeX

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

Lean4

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

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