mul_left_dvd — Mathlib

English

In a commutative monoid, a divides all left associates of b; i.e., a · u ∣ b ↔ a ∣ b.

Русский

В коммутативном моноиде a делит все левые ассоциаты b; то есть a·u ∣ b ↔ a ∣ b.

LaTeX

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

Lean4

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

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