mul_right_dvd — Mathlib

English

Let α be a monoid. For all a, b, u ∈ α, if u is a unit, then a·u divides b if and only if a divides b.

Русский

Пусть α — моноид. Для любых a, b, u ∈ α, если u является единицей, то a·u делится на b тогда и только тогда, когда a делит b.

LaTeX

$$$$\forall a,b,u \in \alpha,\ \operatorname{IsUnit}(u) \Rightarrow (a u \mid b) \Leftrightarrow (a \mid b).$$$$

Lean4

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

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