mem_divisors — Mathlib

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

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