English
For all n, m: n ∈ divisors m iff n ∣ m and m ≠ 0.
Русский
Для всех n,m: n ∈ divisors(m) тогда и только тогда, когда n ∣ m и m ≠ 0.
LaTeX
$$$\forall n\, m,\ n \in \mathrm{divisors}(m) \iff n \mid m \land m \neq 0$$$
Lean4
@[simp]
theorem mem_divisors {m : ℕ} : n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0 :=
by
rcases eq_or_ne m 0 with (rfl | hm); · simp [divisors]
simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter, mem_range, and_iff_right_iff_imp,
Nat.lt_succ_iff]
exact le_of_dvd hm.bot_lt