mul_right_dvd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- In a monoid, an element `a` divides an element `b` iff all associates of `a` divide `b`. -/
theorem mul_right_dvd : a * u ∣ b ↔ a ∣ b :=
  Iff.intro (fun ⟨c, eq⟩ => ⟨↑u * c, eq.trans (mul_assoc _ _ _)⟩) fun h =>
    dvd_trans (Dvd.intro (↑u⁻¹) (by rw [mul_assoc, u.mul_inv, mul_one])) h

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