Int

📁 Source: Mathlib/Data/Nat/Prime/Int.lean

Statistics

Metric	Count
Definitions	0
Theorems prime_ofNat_iff, prime_three, prime_two, pow_inj, pow_inj', prime_iff_prime_int	6
Total	6

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prime_ofNat_iff 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero instCommSemiring Nat.Prime	—	Nat.prime_iff_prime_int
prime_three 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero instCommSemiring	—	prime_ofNat_iff Nat.prime_three
prime_two 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero instCommSemiring	—	prime_ofNat_iff Nat.prime_two

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prime_iff_prime_int 📖	mathematical	—	Prime Prime CommSemiring.toCommMonoidWithZero Int.instCommSemiring	—	Prime.pos Int.isUnit_iff_natAbs_eq Prime.ne_one Prime.dvd_mul prime_iff isUnit_iff cast_one

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pow_inj 📖	—	Nat.Prime Monoid.toNatPow Nat.instMonoid	—	—	dvd_antisymm Nat.instIsCancelMulZero Unique.instSubsingleton dvd_of_dvd_pow dvd_pow_self Nat.pow_right_injective two_le
pow_inj' 📖	—	Nat.Prime Monoid.toNatPow Nat.instMonoid	—	—	—

---

← Back to Index