`IndisputableMonolith.NumberTheory.Primes`

IndisputableMonolith/NumberTheory/Primes.lean · 23 lines · 0 declarations

Explainer status: ready · generated 2026-05-14 10:18:31.167779+00:00

   1import IndisputableMonolith.NumberTheory.Primes.Basic
   2import IndisputableMonolith.NumberTheory.Primes.RSConstants
   3import IndisputableMonolith.NumberTheory.Primes.GCDLCM
   4import IndisputableMonolith.NumberTheory.Primes.Wrappers
   5import IndisputableMonolith.NumberTheory.Primes.Modular
   6import IndisputableMonolith.NumberTheory.Primes.Factorization
   7import IndisputableMonolith.NumberTheory.Primes.Squarefree
   8import IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
   9import IndisputableMonolith.NumberTheory.Primes.Resonance
  10
  11/-!
  12Prime-number namespace aggregator.
  13
  14Prefer importing this module (rather than individual files) from downstream code.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace NumberTheory
  19namespace Primes
  20end Primes
  21end NumberTheory
  22end IndisputableMonolith
  23

source mirrored from github.com/jonwashburn/shape-of-logic