Commit 2023-06-11 13:19 f0892dfd

View on Github →

feat: port NumberTheory.Wilson (#4970)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Wilson.lean

added theorem Nat.prime_iff_fac_equiv_neg_one

added theorem Nat.prime_of_fac_equiv_neg_one

added theorem ZMod.prod_Ico_one_prime

added theorem ZMod.wilsons_lemma