Basic

📁 Source: Mathlib/RingTheory/Int/Basic.lean

Statistics

Metric	Count
Definitions instDecidablePredIrreducible, instDecidablePredPrime	2
Theorems dvd_mul, dvd_mul', dvd_pow, dvd_pow', eq_pow_of_mul_eq_pow_odd, eq_pow_of_mul_eq_pow_odd_left, eq_pow_of_mul_eq_pow_odd_right, exists_prime_and_dvd, gcd_ne_one_iff_gcd_mul_right_ne_one, isCoprime_iff_nat_coprime, natAbs_euclideanDomain_gcd, prime_iff_natAbs_prime, span_natAbs, sq_of_gcd_eq_one, sq_of_isCoprime, prime_two_or_dvd_of_dvd_two_mul_pow_self_two	16
Total	18

Int

Definitions

Name	Category	Theorems
instDecidablePredIrreducible 📖	CompOp	—
instDecidablePredPrime 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_pow_of_mul_eq_pow_odd 📖	—	IsCoprime instCommSemiring Odd Nat.instSemiring Monoid.toNatPow instMonoid	—	—	eq_pow_of_mul_eq_pow_odd_left eq_pow_of_mul_eq_pow_odd_right
eq_pow_of_mul_eq_pow_odd_left 📖	—	IsCoprime instCommSemiring Odd Nat.instSemiring Monoid.toNatPow instMonoid	—	—	exists_associated_pow_of_mul_eq_pow' IsBezout.of_isPrincipalIdealRing EuclideanDomain.to_principal_ideal_domain instIsDomain Associated.symm Odd.neg_pow associated_iff_natAbs
eq_pow_of_mul_eq_pow_odd_right 📖	—	IsCoprime instCommSemiring Odd Nat.instSemiring Monoid.toNatPow instMonoid	—	—	eq_pow_of_mul_eq_pow_odd_left IsCoprime.symm mul_comm
exists_prime_and_dvd 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero instCommSemiring	—	Nat.exists_prime_and_dvd Nat.prime_iff_prime_int natCast_dvd
gcd_ne_one_iff_gcd_mul_right_ne_one 📖	—	—	—	—	—
isCoprime_iff_nat_coprime 📖	mathematical	—	IsCoprime instCommSemiring	—	isCoprime_iff_gcd_eq_one gcd_eq_natAbs
natAbs_euclideanDomain_gcd 📖	mathematical	—	EuclideanDomain.gcd euclideanDomain	—	EuclideanDomain.gcd_dvd_left EuclideanDomain.gcd_dvd_right EuclideanDomain.dvd_gcd
prime_iff_natAbs_prime 📖	mathematical	—	Prime CommSemiring.toCommMonoidWithZero instCommSemiring Nat.Prime	—	Associated.prime_iff associated_natAbs Nat.prime_iff_prime_int
span_natAbs 📖	mathematical	—	Ideal.span instSemiring Set Set.instSingletonSet	—	Ideal.span_singleton_eq_span_singleton instIsDomain Associated.symm associated_natAbs
sq_of_gcd_eq_one 📖	—	Monoid.toNatPow instMonoid	—	—	coe_gcd isUnit_one exists_associated_pow_of_mul_eq_pow units_eq_one_or mul_one mul_neg
sq_of_isCoprime 📖	—	IsCoprime instCommSemiring Monoid.toNatPow instMonoid	—	—	sq_of_gcd_eq_one isCoprime_iff_gcd_eq_one

Int.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_mul 📖	—	Nat.Prime	—	—	Nat.Prime.dvd_mul Int.natCast_dvd
dvd_mul' 📖	—	Nat.Prime	—	—	Int.natCast_dvd dvd_mul
dvd_pow 📖	—	Nat.Prime Monoid.toNatPow Int.instMonoid	—	—	Nat.Prime.dvd_of_dvd_pow Int.natCast_dvd
dvd_pow' 📖	—	Nat.Prime Monoid.toNatPow Int.instMonoid	—	—	Int.natCast_dvd dvd_pow

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prime_two_or_dvd_of_dvd_two_mul_pow_self_two 📖	—	Nat.Prime Monoid.toNatPow Int.instMonoid	—	—	Int.Prime.dvd_mul le_antisymm zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.Prime.two_le Nat.Prime.dvd_mul sq

---

← Back to Index