Commit 2023-06-17 11:16 92e17130

View on Github →

feat: port NumberTheory.LegendreSymbol.QuadraticChar.Basic (#5175)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

added theorem FiniteField.isSquare_neg_one_iff

added def quadraticChar

added def quadraticCharFun

added theorem quadraticCharFun_eq_one_of_char_two

added theorem quadraticCharFun_eq_pow_of_char_ne_two

added theorem quadraticCharFun_eq_zero_iff

added theorem quadraticCharFun_mul

added theorem quadraticCharFun_one

added theorem quadraticCharFun_zero

added theorem quadraticChar_card_sqrts

added theorem quadraticChar_dichotomy

added theorem quadraticChar_eq_neg_one_iff_not_one

added theorem quadraticChar_eq_one_of_char_two

added theorem quadraticChar_eq_pow_of_char_ne_two'

added theorem quadraticChar_eq_pow_of_char_ne_two

added theorem quadraticChar_eq_zero_iff

added theorem quadraticChar_exists_neg_one

added theorem quadraticChar_isNontrivial

added theorem quadraticChar_isQuadratic

added theorem quadraticChar_neg_one

added theorem quadraticChar_neg_one_iff_not_isSquare

added theorem quadraticChar_one_iff_isSquare

added theorem quadraticChar_sq_one'

added theorem quadraticChar_sq_one

added theorem quadraticChar_sum_zero

added theorem quadraticChar_zero