Commit 2023-05-22 19:15 6210e2d9

View on Github →

feat: port NumberTheory.LegendreSymbol.ZModChar (#4205)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean

added theorem ZMod.isQuadratic_χ₄

added theorem ZMod.isQuadratic_χ₈'

added theorem ZMod.isQuadratic_χ₈

added theorem ZMod.neg_one_pow_div_two_of_one_mod_four

added theorem ZMod.neg_one_pow_div_two_of_three_mod_four

added theorem ZMod.test

added def ZMod.χ₄

added theorem ZMod.χ₄_eq_neg_one_pow

added theorem ZMod.χ₄_int_eq_if_mod_four

added theorem ZMod.χ₄_int_mod_four

added theorem ZMod.χ₄_int_one_mod_four

added theorem ZMod.χ₄_int_three_mod_four

added theorem ZMod.χ₄_nat_eq_if_mod_four

added theorem ZMod.χ₄_nat_mod_four

added theorem ZMod.χ₄_nat_one_mod_four

added theorem ZMod.χ₄_nat_three_mod_four

added def ZMod.χ₈'

added theorem ZMod.χ₈'_eq_χ₄_mul_χ₈

added theorem ZMod.χ₈'_int_eq_if_mod_eight

added theorem ZMod.χ₈'_int_eq_χ₄_mul_χ₈

added theorem ZMod.χ₈'_nat_eq_if_mod_eight

added def ZMod.χ₈

added theorem ZMod.χ₈_int_eq_if_mod_eight

added theorem ZMod.χ₈_int_mod_eight

added theorem ZMod.χ₈_nat_eq_if_mod_eight

added theorem ZMod.χ₈_nat_mod_eight