English
Let χ be a multiplicative character that is quadratic. Then its inverse is equal to itself; equivalently χ^(-1) = χ (and hence χ^2 = 1).
Русский
Пусть χ — мультипликативный характер, квадратный. Тогда его обратный образ совпадает с самим χ; то есть χ^{-1} = χ (и, следовательно, χ^2 = 1).
LaTeX
$$$\chi^{-1} = \chi$$$
Lean4
/-- The inverse of a quadratic character is itself. → -/
theorem inv {χ : MulChar R R'} (hχ : χ.IsQuadratic) : χ⁻¹ = χ :=
by
ext x
rw [inv_apply_eq_inv]
rcases hχ x with (h₀ | h₁ | h₂)
· rw [h₀, Ring.inverse_zero]
· rw [h₁, Ring.inverse_one]
· -- Porting note (#11573): was `by norm_cast`
have : (-1 : R') = (-1 : R'ˣ) := by norm_cast; simp
rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ), inv_neg, inv_one]
