Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `odd_of_left`, `odd_of_right`, `coprime_pow_of_not_dvd`, `dvd_iff_eq`, `dvd_iff_not_coprime`, `dvd_mul_of_dvd_ne`, `dvd_of_dvd_pow`, `eq_one_of_pow`, `eq_two_or_odd`, `eq_two_or_odd'`, `even_iff`, `even_sub_one`, `five_le_of_ne_two_of_ne_three`, `mod_two_eq_one_iff_ne_two`, `mul_eq_prime_sq_iff`, `not_coprime_iff_dvd`, `not_dvd_mul`, `not_prime_pow`, `not_prime_pow'`, `odd_of_ne_two`, `pow_eq_iff`, `pred_pos`, `coprime_of_dvd'`, `coprime_of_lt_minFac`, `coprime_of_lt_prime`, `coprime_or_dvd_of_prime`, `coprime_pow_primes`, `coprime_primes`, `coprime_two_left`, `coprime_two_right`, `dvd_of_forall_prime_mul_dvd`, `dvd_prime_pow`, `eq_one_iff_not_exists_prime_dvd`, `eq_or_coprime_of_le_prime`, `eq_prime_pow_of_dvd_least_prime_pow`, `exists_dvd_of_not_prime`, `exists_dvd_of_not_prime2`, `gcd_eq_one_of_lt_minFac`, `ne_one_iff_exists_prime_dvd`, `not_prime_iff_exists_dvd_lt`, `not_prime_iff_exists_dvd_ne`, `not_prime_iff_exists_mul_eq`, `not_prime_mul`, `not_prime_of_dvd_of_lt`, `not_prime_of_dvd_of_ne`, `not_prime_of_mul_eq`, `prime_eq_prime_of_dvd_pow`, `prime_mul_iff`, `succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul`, `succ_pred_prime`, `coprime_two_left`, `coprime_two_right`	52
Total	52

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_of_dvd'` 📖	—	—	—	—	`coprime_of_dvd` `not_le_of_gt` `Prime.one_lt`
`coprime_of_lt_minFac` 📖	—	`minFac`	—	—	`Prime.not_coprime_iff_dvd` `Mathlib.Tactic.Push.not_and_eq` `LT.lt.false` `LE.le.trans_lt` `LT.lt.trans_le` `minFac_le_of_dvd` `Prime.two_le`
`coprime_of_lt_prime` 📖	—	`Prime`	—	—	`coprime_or_dvd_of_prime`
`coprime_or_dvd_of_prime` 📖	—	`Prime`	—	—	`Prime.dvd_iff_not_coprime` `em`
`coprime_pow_primes` 📖	mathematical	`Prime`	`Monoid.toNatPow` `instMonoid`	—	`coprime_primes`
`coprime_primes` 📖	—	`Prime`	—	—	`Prime.coprime_iff_not_dvd` `dvd_prime_two_le` `Prime.two_le`
`coprime_two_left` 📖	mathematical	—	`Odd` `instSemiring`	—	`Prime.coprime_iff_not_dvd` `prime_two` `not_even_iff_odd` `instAtLeastTwoHAddOfNat` `even_iff_two_dvd`
`coprime_two_right` 📖	mathematical	—	`Odd` `instSemiring`	—	`coprime_two_left`
`dvd_of_forall_prime_mul_dvd` 📖	—	—	—	—	`eq_or_ne` `one_dvd` `exists_prime_and_dvd` `trans` `instIsTransDvd` `dvd_mul_left`
`dvd_prime_pow` 📖	mathematical	`Prime`	`Monoid.toNatPow` `instMonoid`	—	`dvd_prime_pow` `instIsCancelMulZero` `prime_iff` `associated_eq_eq` `Unique.instSubsingleton`
`eq_one_iff_not_exists_prime_dvd` 📖	—	—	—	—	`not_iff_not` `ne_one_iff_exists_prime_dvd`
`eq_or_coprime_of_le_prime` 📖	—	`Prime`	—	—	`coprime_of_lt_prime` `LE.le.eq_or_lt`
`eq_prime_pow_of_dvd_least_prime_pow` 📖	—	`Prime` `Monoid.toNatPow` `instMonoid`	—	—	`dvd_prime_pow` `le_antisymm` `not_le` `Prime.one_lt`
`exists_dvd_of_not_prime` 📖	—	`Prime`	—	—	`minFac_dvd` `Prime.one_lt` `minFac_prime` `not_prime_iff_minFac_lt`
`exists_dvd_of_not_prime2` 📖	—	`Prime`	—	—	`minFac_dvd` `Prime.two_le` `minFac_prime` `not_prime_iff_minFac_lt`
`gcd_eq_one_of_lt_minFac` 📖	—	`minFac`	—	—	`coprime_of_lt_minFac`
`ne_one_iff_exists_prime_dvd` 📖	mathematical	—	`Prime`	—	`prime_two` `minFac_prime` `minFac_dvd`
`not_prime_iff_exists_dvd_lt` 📖	mathematical	—	`Prime`	—	`exists_dvd_of_not_prime2` `not_prime_of_dvd_of_lt`
`not_prime_iff_exists_dvd_ne` 📖	mathematical	—	`Prime`	—	`exists_dvd_of_not_prime` `not_prime_of_dvd_of_ne`
`not_prime_iff_exists_mul_eq` 📖	mathematical	—	`Prime`	—	`prime_iff_not_exists_mul_eq`
`not_prime_mul` 📖	mathematical	—	`Prime`	—	—
`not_prime_of_dvd_of_lt` 📖	mathematical	—	`Prime`	—	`not_prime_of_dvd_of_ne`
`not_prime_of_dvd_of_ne` 📖	mathematical	—	`Prime`	—	`Prime.eq_one_or_self_of_dvd`
`not_prime_of_mul_eq` 📖	mathematical	—	`Prime`	—	`not_prime_mul`
`prime_eq_prime_of_dvd_pow` 📖	—	`Prime` `Monoid.toNatPow` `instMonoid`	—	—	`prime_dvd_prime_iff_eq` `Prime.dvd_of_dvd_pow`
`prime_mul_iff` 📖	mathematical	—	`Prime`	—	—
`succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul` 📖	—	`Prime` `Monoid.toNatPow` `instMonoid`	—	—	`pow_add` `Prime.dvd_mul` `pow_succ`
`succ_pred_prime` 📖	—	`Prime`	—	—	`Prime.pos`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`odd_of_left` 📖	mathematical	—	`Odd` `Nat.instSemiring`	—	`Nat.coprime_two_left`
`odd_of_right` 📖	mathematical	—	`Odd` `Nat.instSemiring`	—	`Nat.coprime_two_right`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_pow_of_not_dvd` 📖	mathematical	`Nat.Prime`	`Monoid.toNatPow` `Nat.instMonoid`	—	`coprime_iff_not_dvd`
`dvd_iff_eq` 📖	—	`Nat.Prime`	—	—	`Nat.prime_mul_iff` `mul_one` `dvd_refl`
`dvd_iff_not_coprime` 📖	—	`Nat.Prime`	—	—	`iff_not_comm` `coprime_iff_not_dvd`
`dvd_mul_of_dvd_ne` 📖	—	`Nat.Prime`	—	—	`Nat.coprime_primes`
`dvd_of_dvd_pow` 📖	—	`Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`Prime.dvd_of_dvd_pow` `prime`
`eq_one_of_pow` 📖	—	`Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`not_imp_not` `not_prime_pow'`
`eq_two_or_odd` 📖	—	`Nat.Prime`	—	—	`eq_one_or_self_of_dvd`
`eq_two_or_odd'` 📖	mathematical	`Nat.Prime`	`Odd` `Nat.instSemiring`	—	`eq_two_or_odd`
`even_iff` 📖	mathematical	`Nat.Prime`	`Even`	—	`Nat.instAtLeastTwoHAddOfNat` `even_iff_two_dvd` `Nat.prime_dvd_prime_iff_eq` `Nat.prime_two`
`even_sub_one` 📖	mathematical	`Nat.Prime`	`Even`	—	`odd_of_ne_two` `Nat.instAtLeastTwoHAddOfNat` `two_mul`
`five_le_of_ne_two_of_ne_three` 📖	—	`Nat.Prime`	—	—	—
`mod_two_eq_one_iff_ne_two` 📖	—	`Nat.Prime`	—	—	`eq_two_or_odd`
`mul_eq_prime_sq_iff` 📖	mathematical	`Nat.Prime`	`Monoid.toNatPow` `Nat.instMonoid`	—	`sq` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `ne_zero` `mul_assoc` `Nat.dvd_prime` `mul_one` `dvd_mul` `mul_comm`
`not_coprime_iff_dvd` 📖	mathematical	—	`Nat.Prime`	—	`Nat.minFac_prime` `Dvd.dvd.trans` `Nat.minFac_dvd` `one_lt`
`not_dvd_mul` 📖	—	`Nat.Prime`	—	—	`dvd_mul`
`not_prime_pow` 📖	mathematical	—	`Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`not_prime_pow'` `Nat.two_le_iff`
`not_prime_pow'` 📖	mathematical	—	`Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`not_irreducible_pow`
`odd_of_ne_two` 📖	mathematical	`Nat.Prime`	`Odd` `Nat.instSemiring`	—	`eq_two_or_odd'`
`pow_eq_iff` 📖	mathematical	`Nat.Prime`	`Monoid.toNatPow` `Nat.instMonoid`	—	`eq_one_of_pow` `pow_one`
`pred_pos` 📖	—	`Nat.Prime`	—	—	`one_lt`

Odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_two_left` 📖	—	`Odd` `Nat.instSemiring`	—	—	`Nat.coprime_two_left`
`coprime_two_right` 📖	—	`Odd` `Nat.instSemiring`	—	—	`Nat.coprime_two_right`

---

← Back to Index