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