English
The quadratic character is multiplicative: quadraticCharFun F (a*b) = quadraticCharFun F a · quadraticCharFun F b.
Русский
Квадратичный характер умножения — мультипликативен: квадратичныйCharFun F (a b) = квадратичныйCharFun F a · квадратичныйCharFun F b.
LaTeX
$$$\text{quadraticCharFun } F (a b) = \text{quadraticCharFun } F a \cdot \text{quadraticCharFun } F b$$$
Lean4
/-- The quadratic character is multiplicative. -/
theorem quadraticCharFun_mul (a b : F) : quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b :=
by
by_cases ha : a = 0
·
rw [ha, zero_mul, quadraticCharFun_zero, zero_mul]
-- now `a ≠ 0`
by_cases hb : b = 0
·
rw [hb, mul_zero, quadraticCharFun_zero, mul_zero]
-- now `a ≠ 0` and `b ≠ 0`
have hab := mul_ne_zero ha hb
by_cases hF : ringChar F = 2
· -- case `ringChar F = 2`
rw [quadraticCharFun_eq_one_of_char_two hF ha, quadraticCharFun_eq_one_of_char_two hF hb,
quadraticCharFun_eq_one_of_char_two hF hab, mul_one]
· -- case of odd characteristic
rw [quadraticCharFun_eq_pow_of_char_ne_two hF ha, quadraticCharFun_eq_pow_of_char_ne_two hF hb,
quadraticCharFun_eq_pow_of_char_ne_two hF hab, mul_pow]
rcases FiniteField.pow_dichotomy hF hb with hb' | hb'
· simp only [hb', mul_one, if_true]
· have h := Ring.neg_one_ne_one_of_char_ne_two hF
simp only [hb', mul_neg, mul_one, h, if_false]
rcases FiniteField.pow_dichotomy hF ha with ha' | ha' <;> simp only [ha', h, neg_neg, if_true, if_false]
