Commit 2023-06-26 15:50 b7b1bb20

View on Github →

feat: port NumberTheory.LegendreSymbol.GaussEisensteinLemmas (#5492)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean

added theorem ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id

added theorem ZMod.div_eq_filter_card

added theorem ZMod.eisenstein_lemma

added theorem ZMod.eisenstein_lemma_aux

added theorem ZMod.gauss_lemma

added theorem ZMod.gauss_lemma_aux

added theorem ZMod.sum_mul_div_add_sum_mul_div_eq_mul