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 monoid, an element `a` divides an element `b` iff `a` divides all associates of `b`. -/
theorem dvd_mul_right : a ∣ b * u ↔ a ∣ b :=
Iff.intro (fun ⟨c, eq⟩ ↦ ⟨c * ↑u⁻¹, by rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]⟩) fun ⟨_, eq⟩ ↦
eq.symm ▸ (_root_.dvd_mul_right _ _).mul_right _