mem_properDivisors_iff_exists — Mathlib

English

Let n ≠ 0. Then m ∈ properDivisors(n) iff there exists k > 1 such that n = m k.

Русский

Пусть n ≠ 0. Тогда m ∈ properDivisors(n) тогда и только тогда, когда существует k > 1 такое, что n = m k.

LaTeX

$$$ n \neq 0 \Rightarrow ( m \in n.properDivisors) \iff (\exists k > 1, n = m k)$$$

Lean4

/-- See also `Nat.mem_properDivisors`. -/
theorem mem_properDivisors_iff_exists {m n : ℕ} (hn : n ≠ 0) : m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k :=
  by
  refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
  · exact (Nat.mul_div_cancel' (mem_properDivisors.mp h).1).symm
  · rintro ⟨k, hk, rfl⟩
    rw [mul_ne_zero_iff] at hn
    exact mem_properDivisors.mpr ⟨⟨k, rfl⟩, lt_mul_of_one_lt_right (Nat.pos_of_ne_zero hn.1) hk⟩

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