theorem
proved
prime_three
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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