associated_isUnit_mul_left_iff — Mathlib

English

Let N be a commutative monoid and u a unit. Then for all a, b in N, the relation 'a' is associated with b is equivalent to 'u*a' is associated with b; i.e., left-multiplying by a unit does not change association.

Русский

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

LaTeX

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

Lean4

theorem associated_isUnit_mul_left_iff {N : Type*} [CommMonoid N] {u a b : N} (hu : IsUnit u) :
    Associated (u * a) b ↔ Associated a b := by
  rw [mul_comm]
  exact associated_mul_isUnit_left_iff hu

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