module module

`IndisputableMonolith.NumberTheory.Primes.Modular`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.Primes module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Primes.Basic module_import
IndisputableMonolith.NumberTheory.Primes.RSConstants module_import

declarations in this module (17)

def wheel840 L22
def chi8 L33
theorem chi8_periodic L40
theorem chi8_mod0 L48
theorem chi8_mod1 L52
theorem chi8_mod2 L56
theorem chi8_mod3 L60
theorem chi8_mod4 L64
theorem chi8_mod5 L68
theorem chi8_mod6 L72
theorem chi8_mod7 L76
theorem chi8_eq_zero_iff_even L81
theorem chi8_ne_zero_iff_odd L113
theorem wheel840_accepts L118
theorem prime_dvd_wheel840 L133
theorem wheel840_rejects L157
theorem wheel840_rejects_of_gcd_ne_one L181