theorem
proved
prime_three
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.Basic on GitHub at line 24.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
21theorem prime_two : Nat.Prime 2 := by
22 decide
23
24theorem prime_three : Nat.Prime 3 := by
25 decide
26
27theorem not_prime_zero : ¬ Nat.Prime 0 := by
28 decide
29
30theorem not_prime_one : ¬ Nat.Prime 1 := by
31 decide
32
33/-! ### Local aliases (optional convenience) -/
34
35/-- Repo-local alias for Mathlib’s `Nat.Prime` (kept transparent). -/
36abbrev Prime (n : ℕ) : Prop := Nat.Prime n
37
38@[simp] theorem prime_iff (n : ℕ) : Prime n ↔ Nat.Prime n := Iff.rfl
39
40end Primes
41end NumberTheory
42end IndisputableMonolith