out_dvd_iff — Mathlib

English

Let α be CancelCommMonoidWithZero and NormalizationMonoid α. For a ∈ α and b ∈ Associates α, b.out divides a if and only if b ≤ mk a.

Русский

Пусть α имеет CancelCommMonoidWithZero и NormalizationMonoid. Для a ∈ α и b ∈ Associates α, b.out делит a тогда и только тогда, когда b ≤ mk a.

LaTeX

$$$$ b.out \\mid a \\iff b \\le \\operatorname{mk} a $$$$

Lean4

theorem out_dvd_iff (a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associates.mk a :=
  Quotient.inductionOn b <| by simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

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