associated_unit_mul_right — Mathlib

English

In a commutative monoid, right-multiplying by a unit yields an associated element: a ~ᵤ (u · a).

Русский

В коммутативном моноиде правое умножение на единицу даёт элемент, связанный: a ~ᵤ (u · a).

LaTeX

$$$ \\forall a,u \\in N, \\text{IsUnit } u \\Rightarrow \\text{Associated}(a, u \\cdot a). $$$

Lean4

theorem associated_unit_mul_right {N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) : Associated a (u * a) :=
  (associated_unit_mul_left a u hu).symm

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