Documentation Verification Report

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`, `isCoprime_two_left`, `isCoprime_two_right`, `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`	18
Total	20

Int

Definitions

Name	Category	Theorems
`instDecidablePredIrreducible` 📖	CompOp	—
`instDecidablePredPrime` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_pow_of_mul_eq_pow_odd` 📖	mathematical	`IsCoprime` `instCommSemiring` `Odd` `Nat.instSemiring` `Monoid.toPow` `instMonoid`	`Monoid.toPow` `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` 📖	mathematical	`IsCoprime` `instCommSemiring` `Odd` `Nat.instSemiring` `Monoid.toPow` `instMonoid`	`Monoid.toPow` `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` 📖	mathematical	`IsCoprime` `instCommSemiring` `Odd` `Nat.instSemiring` `Monoid.toPow` `instMonoid`	`Monoid.toPow` `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`
`isCoprime_two_left` 📖	mathematical	—	`IsCoprime` `instCommSemiring` `Odd` `instSemiring`	—	—
`isCoprime_two_right` 📖	mathematical	—	`IsCoprime` `instCommSemiring` `Odd` `instSemiring`	—	—
`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` 📖	mathematical	`Monoid.toPow` `instMonoid`	`Monoid.toPow` `instMonoid`	—	`coe_gcd` `isUnit_one` `exists_associated_pow_of_mul_eq_pow` `units_eq_one_or` `mul_one` `mul_neg`
`sq_of_isCoprime` 📖	mathematical	`IsCoprime` `instCommSemiring` `Monoid.toPow` `instMonoid`	`Monoid.toPow` `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.toPow` `Int.instMonoid`	—	—	`Nat.Prime.dvd_of_dvd_pow` `Int.natCast_dvd`
`dvd_pow'` 📖	—	`Nat.Prime` `Monoid.toPow` `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.toPow` `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