fourierChar_ne_one — Mathlib

English

The Fourier char fourierChar is not the constant function 1.

Русский

Фурье характер fourierChar не является тождественно равной единице.

LaTeX

$$$$ fourierChar \\neq 1 $$$$

Lean4

theorem fourierChar_ne_one : fourierChar ≠ 1 := by
  rw [DFunLike.ne_iff]
  use 2⁻¹
  simp only [fourierChar_apply', AddChar.one_apply]
  rw [mul_comm, ← mul_assoc, inv_mul_cancel₀ (by positivity), one_mul]
  exact Circle.exp_pi_ne_one

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