mem_properDivisors — Mathlib

English

For all m, n ∈ Nat, n ∈ properDivisors(m) if and only if n ∣ m and n < m.

Русский

Для всех m, n ∈ Nat, n ∈ properDivisors(m) тогда и только тогда, когда n ∣ m и n < m.

LaTeX

$$$\forall m\in\mathbb{N},\ \ n \in \mathrm{properDivisors}(m) \iff n \mid m \land n < m$$$

Lean4

@[simp]
theorem mem_properDivisors {m : ℕ} : n ∈ properDivisors m ↔ n ∣ m ∧ n < m :=
  by
  rcases eq_or_ne m 0 with (rfl | hm); · simp [properDivisors]
  simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]

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