IndisputableMonolith.NumberTheory.Primes.Factorization

declarations in this module (19)

• def vp L21
• theorem vp_def L23
• theorem factorization_mul L28
• theorem factorization_pow L33
• theorem vp_mul L37
• theorem vp_pow L42
• theorem vp_zero L50
• theorem vp_one L54
• theorem vp_prime_self L58
• theorem vp_prime_ne L63
• theorem vp_prime_pow L70
• theorem vp_prime_pow_ne L77
• theorem vp_gcd L88
• theorem vp_lcm L96
• theorem vp_eq_of_eq_prime_pow L105
• theorem vp_eq_zero_of_eq_prime_pow_ne L111
• theorem pow_dvd_iff_le_vp L121
• theorem vp_eq_zero_of_not_dvd L128
• theorem prime_dvd_iff_vp_pos L133