χ₄ — Mathlib

English

The function χ₄ on Z/4Z is a nontrivial quadratic character taking values in {0,1,-1}.

Русский

Функция χ₄ на Z/4Z является ненулевым квадратическим образом, принимающим значения в {0,1,-1}.

LaTeX

$$$ χ_{4} : \\mathbb{Z}/4\\mathbb{Z} \\to \\mathbb{Z} \\text{ is a quadratic character } χ_{4}(n) \\in \\{0,1,-1\\}. $$$

Lean4

/-- Define the nontrivial quadratic character on `ZMod 4`, `χ₄`.
It corresponds to the extension `ℚ(√-1)/ℚ`. -/
@[simps]
def χ₄ : MulChar (ZMod 4) ℤ
    where
  toFun
    a :=
    match a with
    | 0 | 2 => 0
    | 1 => 1
    | 3 => -1
  map_one' := rfl
  map_mul' := by decide
  map_nonunit' := by decide

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