of_mul_left — Mathlib

English

If a*b is associated to c*d and a is associated to c and a ≠ 0, then b is associated to d.

Русский

Если a*b ассоциировано с c*d и a ассоциировано с c, и a ≠ 0, тогда b ассоциирован с d.

LaTeX

$$$$\mathrm{Associated}(a\cdot b, c\cdot d) \land \mathrm{Associated}(a,c) \land a \neq 0 \Rightarrow \mathrm{Associated}(b,d).$$$$

Lean4

theorem of_mul_left [CancelCommMonoidWithZero M] {a b c d : M} (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) :
    b ~ᵤ d :=
  let ⟨u, hu⟩ := h
  let ⟨v, hv⟩ := Associated.symm h₁
  ⟨u * (v : Mˣ),
    mul_left_cancel₀ ha
      (by
        rw [← hv, mul_assoc c (v : M) d, mul_left_comm c, ← hu]
        simp [hv.symm, mul_comm, mul_left_comm])⟩

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