Refactor elementary number theory

[EgbertRijke]

The biggest changes come from a change in the definition of the quotient of a divisible natural number. The updated definition defines the quotient of n by d, provided that d | n is the unique natural number q ≤ n such that q * d = n. This change prevents some case analyses around the situation where the Curry-Howard interpretation of divisibility is not a proposition. An alternative definition of divisibility is also given: bounded divisibility. This is always a proposition. The poset of the natural numbers by divisibility is updated to use bounded divisibility in favor of propositional truncation.

The change in the definition of the quotient by divisibility triggered changes in the fundamental theorem of arithmetic, which is thoroughly revised after discovering that the strong induction that we previously used was unnecessarily complicated.

New files include:

• Bounded divisibility
• Irrationality of the square root of 2
• Lists of prime numbers
• Multiplicative decompositions of natural numbers
• Nicomachus's Theorem
• Nontrivial divisors of natural numbers
• Number of divisors
• Parity of integers
• Pronic numbers
• Square pyramidal numbers
• Unit integers
• Unit similarity integers
• Well-ordering principles of the integers
• Dependent lists
• Elementhood relation on lists
• Universal quantification on lists

[fredrik-bakke]

Cool! I'll wait to submit the 100-theorems list to Freek until after this PR is merged :) #1203

[fredrik-bakke]

Are you still planning to formalize the irrationality of 2 as part of this PR?

[EgbertRijke]

Are you still planning to formalize the irrationality of 2 as part of this PR?

Yes, definitely.

I want to do it well, improving the infrastructure for divisibility of integers and setting up infrastructure for parity of integers. My changes to the divisibility of natural numbers led me to refactor a bunch of definitions depending on it, but at the end of this formalization in elementary number theory should feel a lot less ad-hoc.

[fredrik-bakke]

That's very nice. This namespace is well-deserving of some love and attention!

[EgbertRijke]

I'm teaching a course on elementary number theory this semester, and I want to formalize some of it as I go.