expect_apply_eq_zero_iff_ne_zero — Mathlib

English

For a finite α and a ∈ α, the expectation over additive characters of a being zero is equivalent to a ≠ 0: 𝔼[ψ(a) = 0] iff a ≠ 0.

Русский

Для конечной группы α и элемента a ∈ α математическое ожидание по всем аддитивным символам ψ: α → ℂ равно 0 тогда и только тогда, когда a ≠ 0.

LaTeX

$$$$ \\mathbb{E}_{\\psi}[\\psi(a) = 0] \\;\\leftrightarrow\\; a \\neq 0. $$$$

Lean4

theorem expect_apply_eq_zero_iff_ne_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
  classical
  cases nonempty_fintype α
  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]

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