associated_mul_isUnit_left_iff — Mathlib

English

If u is a unit, then Associated (a·u) b is equivalent to Associated a b.

Русский

Если u — единица, то Associated (a·u) b эквивалентно Associated a b.

LaTeX

$$$\\text{IsUnit } u \\Rightarrow (\\text{Associated}(a \\cdot u, b) \\iff \\text{Associated}(a, b)).$$$

Lean4

theorem associated_mul_isUnit_left_iff {N : Type*} [Monoid N] {a u b : N} (hu : IsUnit u) :
    Associated (a * u) b ↔ Associated a b :=
  ⟨(associated_mul_unit_right _ _ hu).trans, (associated_mul_unit_left _ _ hu).trans⟩

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