expect_apply_ne_zero_iff_eq_zero — Mathlib

English

For a finite α and a ∈ α, the expectation 𝔼[ψ(a)] is nonzero exactly when a = 0.

Русский

Для конечной группы α и элемента a суммарное ожидаемое значение 𝔼[ψ(a)] отлично от нуля тогда и только тогда, когда a = 0.

LaTeX

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

Lean4

theorem expect_apply_ne_zero_iff_eq_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
  expect_apply_eq_zero_iff_ne_zero.not_left

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