dvd_mul_left — Mathlib

English

In a commutative monoid, a divides u · b iff a divides b for a unit u.

Русский

В коммутативном моноиде a делит u·b тогда и только тогда, когда делит b для единицы u.

LaTeX

$$$ a \mid u \cdot b \iff a \mid b $$$

Lean4

/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
associates of `b`. -/
theorem dvd_mul_left : a ∣ u * b ↔ a ∣ b := by
  rw [mul_comm]
  apply dvd_mul_right

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