Commit 2023-06-27 17:19 0285b69b

View on Github →

feat: port NumberTheory.LegendreSymbol.JacobiSymbol (#5502)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

added theorem ZMod.isSquare_of_jacobiSym_eq_one

added theorem ZMod.nonsquare_iff_jacobiSym_eq_neg_one

added theorem ZMod.nonsquare_of_jacobiSym_eq_neg_one

added theorem jacobiSym.at_neg_one

added theorem jacobiSym.at_neg_two

added theorem jacobiSym.at_two

added theorem jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one

added theorem jacobiSym.eq_one_or_neg_one

added theorem jacobiSym.eq_zero_iff

added theorem jacobiSym.eq_zero_iff_not_coprime

added theorem jacobiSym.legendreSym.to_jacobiSym

added theorem jacobiSym.list_prod_left

added theorem jacobiSym.list_prod_right

added theorem jacobiSym.mod_left'

added theorem jacobiSym.mod_left

added theorem jacobiSym.mod_right'

added theorem jacobiSym.mod_right

added theorem jacobiSym.mul_left

added theorem jacobiSym.mul_right'

added theorem jacobiSym.mul_right

added theorem jacobiSym.one_left

added theorem jacobiSym.one_right

added theorem jacobiSym.pow_left

added theorem jacobiSym.pow_right

added theorem jacobiSym.prime_dvd_of_eq_neg_one

added theorem jacobiSym.quadratic_reciprocity'

added theorem jacobiSym.quadratic_reciprocity

added theorem jacobiSym.quadratic_reciprocity_one_mod_four'

added theorem jacobiSym.quadratic_reciprocity_one_mod_four

added theorem jacobiSym.quadratic_reciprocity_three_mod_four

added theorem jacobiSym.sq_one'

added theorem jacobiSym.sq_one

added theorem jacobiSym.trichotomy

added theorem jacobiSym.value_at

added theorem jacobiSym.zero_left

added theorem jacobiSym.zero_right

added def jacobiSym

added theorem qrSign.eq_iff_eq

added theorem qrSign.mul_left

added theorem qrSign.mul_right

added theorem qrSign.neg_one_pow

added theorem qrSign.sq_eq_one

added def qrSign