NatPrime

📁 Source: Mathlib/Data/Int/NatPrime.lean

Statistics

Metric	Count
Definitions	0
Theorems dvd_natAbs_of_coe_dvd_sq, not_prime_of_int_mul, succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul	3
Total	3

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_prime_of_int_mul 📖	mathematical	—	Nat.Prime	—	Nat.not_prime_of_mul_eq
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul 📖	—	Nat.Prime Monoid.toNatPow Nat.instMonoid	—	—	Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

Int.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_natAbs_of_coe_dvd_sq 📖	—	Nat.Prime Monoid.toNatPow Int.instMonoid	—	—	Nat.Prime.dvd_of_dvd_pow sq Int.natCast_dvd

---

← Back to Index