quadraticChar_sq_one' — Mathlib

English

For nonzero a, the value on a square is 1: χ(a^2) = 1 when a ≠ 0.

Русский

Для ненулевого a значение на квадрате равно 1: χ(a^2) = 1 при a ≠ 0.

LaTeX

$$$a\neq 0 \Rightarrow χ(a^2)=1$$$

Lean4

/-- The quadratic character takes the value `1` on nonzero squares. -/
theorem quadraticChar_sq_one' {a : F} (ha : a ≠ 0) : quadraticChar F (a ^ 2) = 1 := by
  simp only [quadraticChar_apply, quadraticCharFun, sq_eq_zero_iff, ha, IsSquare.sq, if_true, if_false]

Похожие утверждения