NtLean.lean

-- NtLean.lean -- root module of the NtLean elementary number theory library.
-- Importing `NtLean` pulls in every chapter of the library.
--
-- Chapters:
--   NtLean.Preamble     the shared Mathlib import surface (see that file for why)
--   NtLean.Basic        conventions, parity, elementary divisibility, gcd warm-ups
--   NtLean.Congruence   the Nat.ModEq API, worked congruence computations, CRT
--   NtLean.Divisibility Bezout, coprimality, Euclid's lemma
--   NtLean.Primes       primality basics, infinitude of primes, concrete primes
--   NtLean.Fibonacci    Fibonacci as a strong divisibility sequence
--   NtLean.Chebyshev    Chebyshev polynomials via the conic c^2 + s^2 = 1
--
-- Results are promoted here from Scratch/Current.lean once they compile cleanly.

import NtLean.Preamble
import NtLean.Basic
import NtLean.Congruence
import NtLean.Divisibility
import NtLean.Primes
import NtLean.Fibonacci
import NtLean.Chebyshev