Nat.prime_of_fac_equiv_neg_one
theorem Nat.prime_of_fac_equiv_neg_one : ∀ {n : ℕ}, ↑(n - 1).factorial = -1 → n ≠ 1 → n.Prime
The theorem `Nat.prime_of_fac_equiv_neg_one` states that for a natural number `n` that is not equal to 1, if the factorial of `(n-1)` is congruent to `-1` modulo `n`, then `n` must be a prime number. In mathematical terms, this theorem says that if $(n-1)! ≡ -1 \mod n$ and $n ≠ 1$, then `n` is a prime number.
More concisely: If $(n-1)!\equiv -1\ (\mod\ n)$ and $n\neq 1$, then $n$ is prime.
|
ZMod.wilsons_lemma
theorem ZMod.wilsons_lemma : ∀ (p : ℕ) [inst : Fact p.Prime], ↑(p - 1).factorial = -1
**Wilson's Lemma**: This theorem states that for any prime number `p`, the factorial of `p - 1` is congruent to `-1` modulo `p`. In other words, when you multiply all the integers from `1` to `p - 1` together and you then divide that product by `p`, the remainder is `-1`. This is a fundamental result in number theory, and it's known as Wilson's Lemma.
More concisely: Wilson's Lemma states that for a prime number `p`, (p-1)! ± 1 is congruent to 0 modulo p.
|
Nat.prime_iff_fac_equiv_neg_one
theorem Nat.prime_iff_fac_equiv_neg_one : ∀ {n : ℕ}, n ≠ 1 → (n.Prime ↔ ↑(n - 1).factorial = -1)
The Wilson's Theorem states that for a natural number `n` that is not equal to 1, the factorial of `(n-1)` is congruent to `-1` modulo `n` if and only if `n` is a prime number. In other words, a number `n` is prime if and only if the factorial of its predecessor is equal to `-1` when taken modulo `n`.
More concisely: Wilson's Theorem: A natural number `n` is prime if and only if (n-1)! ± 1 is congruent to 0 modulo n.
|