Fractions and the rationals ℚ

Divisions can leave fractions; the rationals ℚ are the number world that contains them.

Start with a concrete example

Cut one cake into four equal pieces. Three pieces make 3/4. Fractions of whole numbers, with a nonzero denominator, are rational numbers; the fraction need not be a whole number.

A small check: try the idea

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

Is 3/4 a rational number even though it is not an integer?

Read the answer and reasoning

Yes. It is a fraction of integers with a nonzero denominator. A cake cut into four equal pieces makes this concrete.

Build the idea in three steps

Two divisions appear in the Frey coefficient formulas: by 4 and by 16. A division can leave a fraction, and fractions are the everyday example of rational numbers.
The rationals ℚ are quotients of integers. Every integer is a rational number with denominator one, so a statement proved over ℚ automatically says something about each integer as well.
The same equation can be read over different coefficient types. One stored form keeps the Frey coefficients as integers; the sibling switches the coefficient type to ℚ. The proof chooses the type deliberately.

A small example

The fraction −7/4 is not an integer, yet it is a definite rational number. Whether a ÷4 formula stays inside ℤ is a question that has to be tracked field by field.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean

83def freyCurveInt (P : FreyPackage) : WeierstrassCurve ℤ where84  a₁ := 185  a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 486  a₃ := 087  a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 1688  a₆ := 0

How to read this Lean

The shown fields divide by 4 and 16 with the integer type ℤ. The sibling freyCurve, further down in the same file, writes the same five formulas with coefficient type ℚ, where a division always names a genuine rational number without an exactness condition.

Original source ↗ · L83–88 Open the complete saved source

Where this idea is used

5. The suspicious parcel

Fractions and the rationals ℚ

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