mul_left_dvd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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