eq_one_iff — Mathlib

English

A character χ equals the trivial character if and only if χ(a) = 1 for every unit a ∈ R^×.

Русский

Характер χ равен тривиальному тогда и только тогда, когда χ(a) = 1 для каждого единичного элемента a ∈ R^×.

LaTeX

$$$$ \\chi = 1 \\quad \\text{iff} \\quad \\forall a \\in R^\\times,\\; \\chi(a) = 1. $$$$

Lean4

theorem eq_one_iff {χ : MulChar R R'} : χ = 1 ↔ ∀ a : Rˣ, χ a = 1 := by simp only [MulChar.ext_iff, one_apply_coe]

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