eq_one_iff_not_exists_prime_dvd — Mathlib

English

For every n, n = 1 iff for all primes p, p ∤ n.

Русский

Для каждого n: n = 1 тогда и только тогда, когда ни одно простое p не делит n.

LaTeX

$$$$ \forall n \in \mathbb{N},\ n = 1 \iff \forall p \in \mathbb{N},\ p \text{ prime} \rightarrow \lnot(p \mid n). $$$$

Lean4

theorem eq_one_iff_not_exists_prime_dvd {n : ℕ} : n = 1 ↔ ∀ p : ℕ, p.Prime → ¬p ∣ n := by
  simpa using not_iff_not.mpr ne_one_iff_exists_prime_dvd

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