theorem
proved
prime_two
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 21.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
18
19/-! ### Sanity checks (compile-time smoke) -/
20
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