Fermat

📁 Source: Mathlib/NumberTheory/Fermat.lean

Statistics

Metric	Count
Definitions fermatNumber	1
Theorems fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, coprime_fermatNumber_fermatNumber, fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, fermatNumber_eq_prod_add_two, fermatNumber_injective, fermatNumber_mono, fermatNumber_ne_one, fermatNumber_one, fermatNumber_strictMono, fermatNumber_succ, fermatNumber_two, fermatNumber_zero, fermat_primeFactors_one_lt, odd_fermatNumber, pairwise_coprime_fermatNumber, pepin_primality, pepin_primality', pow_of_pow_add_prime, pow_pow_add_primeFactors_one_lt, prime_of_pow_sub_one_prime, prod_fermatNumber, three_le_fermatNumber, two_lt_fermatNumber, two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq	24
Total	25

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq 📖	mathematical	—	Nat.fermatNumber Monoid.toNatPow instMonoid	—	Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq Nat.cast_sub Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq Nat.instAtLeastTwoHAddOfNat Nat.cast_pow Nat.cast_add Nat.cast_one add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.cast_mul AddGroup.toOrderedSub covariant_swap_add_of_covariant_add instAddLeftMono

Nat

Definitions

Name	Category	Theorems
fermatNumber 📖	CompOp	17 math math: odd_fermatNumber, fermatNumber_two, fermatNumber_zero, fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, prod_fermatNumber, two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq, Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq, pairwise_coprime_fermatNumber, fermatNumber_injective, coprime_fermatNumber_fermatNumber, fermatNumber_strictMono, two_lt_fermatNumber, fermatNumber_eq_prod_add_two, three_le_fermatNumber, fermatNumber_mono, fermatNumber_one, fermatNumber_succ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_fermatNumber_fermatNumber 📖	mathematical	—	fermatNumber	—	Dvd.dvd.trans Finset.dvd_prod_of_mem Finset.mem_range fermatNumber_eq_prod_add_two dvd_prime prime_two Odd.not_two_dvd_nat odd_fermatNumber
fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq 📖	mathematical	—	fermatNumber Monoid.toNatPow instMonoid	—	instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.RingNF.nat_rawCast_1 add_zero pow_one mul_one Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow
fermatNumber_eq_prod_add_two 📖	mathematical	—	fermatNumber Finset.prod instCommMonoid Finset.range	—	prod_fermatNumber le_of_lt two_lt_fermatNumber
fermatNumber_injective 📖	mathematical	—	fermatNumber	—	StrictMono.injective fermatNumber_strictMono
fermatNumber_mono 📖	mathematical	—	Monotone instPreorder fermatNumber	—	StrictMono.monotone fermatNumber_strictMono
fermatNumber_ne_one 📖	—	—	—	—	three_le_fermatNumber
fermatNumber_one 📖	mathematical	—	fermatNumber	—	—
fermatNumber_strictMono 📖	mathematical	—	StrictMono instPreorder fermatNumber	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instAtLeastTwoHAddOfNat one_lt_two instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
fermatNumber_succ 📖	mathematical	—	fermatNumber Monoid.toNatPow instMonoid	—	fermatNumber.eq_1 pow_succ mul_comm pow_mul' add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
fermatNumber_two 📖	mathematical	—	fermatNumber	—	—
fermatNumber_zero 📖	mathematical	—	fermatNumber	—	—
fermat_primeFactors_one_lt 📖	mathematical	Prime fermatNumber	Monoid.toNatPow instMonoid	—	Odd.ne_two_of_dvd_nat instAtLeastTwoHAddOfNat Even.add_one even_pow even_two pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE instStarOrderedRing two_ne_zero pow_pow_add_primeFactors_one_lt add_assoc pow_add mul_assoc MulZeroClass.mul_zero zero_add ZMod.exists_sq_eq_two_iff ZMod.natCast_eq_zero_iff cast_add cast_one cast_pow ZMod.natCast_val NeZero.of_gt' instCanonicallyOrderedAdd Prime.one_lt' ZMod.cast_id pow_mul sq fermatNumber.eq_1
odd_fermatNumber 📖	mathematical	—	Odd instSemiring fermatNumber	—	Even.add_one instAtLeastTwoHAddOfNat even_pow even_two LT.lt.ne' pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono instZeroLEOneClass two_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
pairwise_coprime_fermatNumber 📖	mathematical	—	Pairwise fermatNumber	—	coprime_fermatNumber_fermatNumber
pepin_primality 📖	mathematical	ZMod fermatNumber Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instAtLeastTwoHAddOfNat instMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	Prime	—	instAtLeastTwoHAddOfNat two_lt_fermatNumber lucas_primality pow_succ pow_mul neg_one_sq prime_dvd_prime_iff_eq prime_two Prime.dvd_of_dvd_pow two_pos instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid ZMod.neg_one_ne_one
pepin_primality' 📖	mathematical	ZMod fermatNumber Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instAtLeastTwoHAddOfNat NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	Prime	—	instAtLeastTwoHAddOfNat pepin_primality fermatNumber.eq_1 add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
pow_of_pow_add_prime 📖	—	Prime Monoid.toNatPow instMonoid	—	—	exists_eq_two_pow_mul_odd pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE instStarOrderedRing two_ne_zero Odd.nat_add_dvd_pow_add_pow AddRightCancelSemigroup.toIsRightCancelAdd Prime.dvd_iff_eq pow_mul LT.lt.ne' one_pow mul_one
pow_pow_add_primeFactors_one_lt 📖	—	Prime Monoid.toNatPow instMonoid	—	—	lt_of_le_of_ne Prime.two_le eq_neg_iff_add_eq_zero cast_zero cast_add cast_pow cast_one ZMod.natCast_eq_zero_iff one_ne_zero NeZero.one ZMod.nontrivial Prime.one_lt' zero_eq_neg zero_pow pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE instStarOrderedRing two_ne_zero orderOf_eq_prime_pow fact_prime_two ZMod.neg_one_ne_one pow_succ pow_mul neg_one_sq mul_comm Prime.one_le ZMod.orderOf_dvd_card_sub_one
prime_of_pow_sub_one_prime 📖	—	Prime Monoid.toNatPow instMonoid	—	—	tsub_pos_iff_lt instCanonicallyOrderedAdd instOrderedSub Prime.pos LT.lt.ne' LT.lt.trans one_pos instZeroLEOneClass Mathlib.Tactic.Contrapose.contrapose₂ sub_dvd_pow_sub_pow pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Prime.dvd_iff_eq LT.lt.le one_pow prime_def two_le_iff pow_right_injective le_rfl Prime.eq_one_or_self_of_dvd pow_mul
prod_fermatNumber 📖	mathematical	—	Finset.prod instCommMonoid Finset.range fermatNumber	—	Finset.prod_range_succ fermatNumber.eq_1 mul_comm sq_sub_sq instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow add_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one
three_le_fermatNumber 📖	mathematical	—	fermatNumber	—	fermatNumber_mono
two_lt_fermatNumber 📖	mathematical	—	fermatNumber	—	three_le_fermatNumber
two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq 📖	mathematical	—	Monoid.toNatPow instMonoid fermatNumber	—	add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one add_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.RingNF.add_assoc_rev

---

← Back to Index