module module

`IndisputableMonolith.NumberTheory.Primes.Wrappers`

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 (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.Primes.Basic module_import

declarations in this module (9)

theorem exists_prime_ge L21
theorem prime_dvd_mul_iff L27
theorem euclid_lemma L31
theorem prime_dvd_of_dvd_pow L37
theorem prime_eq_of_dvd_pow L41
theorem dvd_prime_pow_iff L49
theorem coprime_iff_not_dvd_of_prime L55
theorem coprime_comm_iff_not_dvd_of_prime L61
theorem prime_dvd_iff_gcd_eq L67