Prime numbers

A prime is at least two and has no positive divisors except one and itself.

Start with a concrete example

Arrange 6 sweets in equal rows: 1×6 and 2×3 both work. For 5 sweets, only 1×5 works (apart from reversing the rows). That is why 5 is prime and 6 is not.

A small check: try the idea

Think with the concrete example above. You can try again.

Is 6 prime?

Read the answer and reasoning

No; 6=2×3. Six sweets fit in two rows of three. A prime has no such factorization with both factors greater than 1.

Build the idea in three steps

A divisor divides a number exactly, without a remainder.
A prime has exactly two positive divisors: one and itself. It must therefore be at least two.
Splitting an exponent into prime factors helps reduce FLT to fewer kinds of cases; the exponent-four case also has a separate role.

A small example

5 is prime. 6 is not: 6 = 2 × 3. One is not prime.

Lean definition · original excerpt

Mathlib · db584cd · Defs.lean

42def Prime (p : ℕ) :=43  Irreducible p44

How to read this Lean

The library defines Nat.Prime through the predicate Irreducible on natural numbers. Here that means a number with no nontrivial multiplicative factorization; it is distinct from irreducibility of a representation.

Original source ↗ · L42–44 Open the complete saved source

Where this idea is used

1. The impossible order 2. The case of three 3. Too many suspects 4. The suitcase diet 5. The suspicious parcel 6. The scissors incident 7. The veterans’ cabinet 8. The secret duet 9. Two doors to the concert 10. A three-note audition 11. Borrow a better passport 12. The workshops agree 13. Pip’s impossible quilt 14. The shrinking reservation 15. The concert of absolute silence 16. The room with no room

Prime numbers

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue