English
A multiplicative character χ into a domain is quadratic if and only if χ^2 = 1.
Русский
Квадратичный характер ⇔ χ^2 = 1.
LaTeX
$$IsQuadratic χ ⇔ χ^2 = 1$$
Lean4
/-- A multiplicative character `χ` into an integral domain is quadratic
if and only if `χ^2 = 1`. -/
theorem isQuadratic_iff_sq_eq_one {M R : Type*} [CommMonoid M] [CommRing R] [NoZeroDivisors R] [Nontrivial R]
{χ : MulChar M R} : IsQuadratic χ ↔ χ ^ 2 = 1 :=
by
refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩
· rw [one_apply_coe, χ.pow_apply_coe]
rcases h x with H | H | H
· exact (not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim
· simp only [H, one_pow]
· simp only [H, even_two, Even.neg_pow, one_pow]
· by_cases hx : IsUnit x
· refine .inr <| sq_eq_one_iff.mp ?_
rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
· exact .inl <| map_nonunit χ hx
