`not_prime_one`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.Basic
domain: NumberTheory
line: 30 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.Primes.Basic on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.