associated_unit_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem associated_unit_mul_left {N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) : Associated (u * a) a :=
  by
  rw [mul_comm]
  exact associated_mul_unit_left _ _ hu

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