Wilson

📁 Source: Mathlib/NumberTheory/Wilson.lean

Statistics

Metric	Count
Definitions	0
Theorems prime_iff_fac_equiv_neg_one, prime_of_fac_equiv_neg_one, prod_Ico_one_prime, wilsons_lemma	4
Total	4

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prime_iff_fac_equiv_neg_one 📖	mathematical	—	Prime ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing factorial NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	—	ZMod.wilsons_lemma prime_of_fac_equiv_neg_one
prime_of_fac_equiv_neg_one 📖	mathematical	ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing factorial NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	Prime	—	eq_or_ne Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natSub Mathlib.Meta.NormNum.isNat_ofNat cast_one Mathlib.Meta.NormNum.isInt_eq_false ZMod.charZero Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_neg two_le_iff exists_dvd_of_not_prime2 dvd_factorial pos_of_gt instCanonicallyOrderedAdd LT.lt.ne' Dvd.dvd.trans ZMod.natCast_eq_zero_iff cast_add neg_add_cancel

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_Ico_one_prime 📖	mathematical	—	Finset.prod ZMod CommRing.toCommMonoid commRing Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	—	Nat.Prime.pos Fact.out Finset.prod_natCast Finset.prod_Ico_id_eq_factorial wilsons_lemma
wilsons_lemma 📖	mathematical	—	ZMod AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField Nat.factorial NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne	—	NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Finset.prod_Ico_id_eq_factorial Finset.prod_natCast Nat.Prime.pos Fact.out Finset.prod_bij Finset.mem_Ico val_zero Units.ne_zero nontrivial val_injective val_lt Units.ext_iff pos_iff_ne_zero val_cast_of_lt Finset.mem_univ natCast_val cast_id Finset.prod_congr map_prod MonoidHom.instMonoidHomClass FiniteField.prod_univ_units_id_eq_neg_one instIsDomain

---

← Back to Index