funlean.
Step 4 / 64

Middle school

Common factors and coprimality

Coprime numbers share no positive divisor larger than one.

Start with a concrete example

The positive divisors of 8 are 1,2,4,8; those of 9 are 1,3,9. Only 1 is shared. “Coprime” describes this pair; it does not mean each number is prime.

A small check: try the idea

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

Are 8 and 9 coprime?

Read the answer and reasoning

Yes; their only shared positive divisor is 1. List the divisors: 8 has 1,2,4,8; 9 has 1,3,9. “Coprime” is about the shared divisors of the pair.

Build the idea in three steps

  1. A common divisor divides both numbers. The greatest common divisor is written gcd.
  2. Coprime means that gcd is one. Neither number has to be prime.
  3. Removing a shared factor simplifies a hypothetical solution, but the proof must keep the equation and nonzero conditions.

A small example

8 and 9 are coprime, although neither is prime. The gcd of 6 and 9 is 3.

Use in Lean · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean

  hgcdab : gcd a b = 1

How to read this Lean

The package field hgcdab records this gcd-one condition for the integers a and b. It is a required proof field.

Original source ↗ · L34–34Open the complete saved source

Where this idea is used

2. The case of three4. The suitcase diet5. The suspicious parcel7. The veterans’ cabinet8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation
I’m lost · Help

Mika’s help desk

Common factors and coprimality

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Coprime numbers share no positive divisor larger than one.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

8 and 9 are coprime, although neither is prime. The gcd of 6 and 9 is 3.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →