dvd_mul_right — 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 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 _

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