dvd_iff — Mathlib

English

In a GroupWithZero, for any m,n, m divides n if and only if m = 0 implies n = 0.

Русский

В группе с нулём для любых m,n верно: m делит n тогда и только если m = 0 предполагает n = 0.

LaTeX

$$$m \\mid n \\iff (m = 0 \\to n = 0)$$$

Lean4

/-- `∣` is not a useful definition if an inverse is available. -/
@[simp]
theorem dvd_iff {m n : α} : m ∣ n ↔ (m = 0 → n = 0) :=
  by
  refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩
  · simp [hm, ha]
  · refine ⟨m⁻¹ * n, ?_⟩
    obtain rfl | hn := eq_or_ne n 0
    · simp
    · rw [mul_inv_cancel_left₀ (mt h hn)]

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