quadraticChar_eq_zero_iff — Mathlib

English

For every a in F, the quadratic character χ satisfies χ(a) = 0 if and only if a = 0.

Русский

Для каждого элемента a из F выполняется χ(a) = 0 тогда и только тогда, когда a = 0.

LaTeX

$$$\\forall a\\in F,\quad χ(a)=0 \\iff a=0$$$

Lean4

/-- The value of the quadratic character on `a` is zero iff `a = 0`. -/
theorem quadraticChar_eq_zero_iff {a : F} : quadraticChar F a = 0 ↔ a = 0 :=
  quadraticCharFun_eq_zero_iff

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