dvd_mul_left — Mathlib

English

In a commutative monoid, if u is a unit, then a divides u·b iff a divides b.

Русский

В коммутативном моноиде, если u — единица, то a делит u·b тогда и только тогда, когда a делит b.

LaTeX

$$$$\operatorname{IsUnit}(u) \Rightarrow (a \mid u b) \Leftrightarrow (a \mid b).$$$$

Lean4

/-- In a commutative monoid, an element `a` divides an element `b` iff `a` divides all left
associates of `b`. -/
@[simp]
theorem dvd_mul_left (hu : IsUnit u) : a ∣ u * b ↔ a ∣ b :=
  by
  rcases hu with ⟨u, rfl⟩
  apply Units.dvd_mul_left

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