Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-10 20:00 c471da71

View on Github →

chore(number_theory/legendre_symbol/gauss_eisenstein_lemmas): move zmod.wilsons_lemma (#19172)

Estimated changes

Modified src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean

deleted theorem zmod.prod_Ico_one_prime

deleted theorem zmod.wilsons_lemma

Modified src/number_theory/wilson.lean

added theorem zmod.prod_Ico_one_prime

added theorem zmod.wilsons_lemma