of_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_mul_right [CancelCommMonoidWithZero M] {a b c d : M} : a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c := by
  rw [mul_comm a, mul_comm c]; exact Associated.of_mul_left

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