exists_apply_ne_zero — Mathlib

English

There exists a character ψ with ψ(a) ≠ 1 if and only if a ≠ 0.

Русский

Существует символ ψ such that ψ(a) ≠ 1 тогда и только тогда a ≠ 0.

LaTeX

$$$ \exists \psi: AddChar(\alpha, \mathbb{C}), \psi(a) \neq 1 \quad\iff\quad a \neq 0 $$$

Lean4

theorem exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 :=
  by
  refine ⟨?_, fun ha ↦ ?_⟩
  · rintro ⟨ψ, hψ⟩ rfl
    exact hψ ψ.map_zero_eq_one
  classical
  by_contra! h
  let f : α → ℂ := fun b ↦ if a = b then 1 else 0
  have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
  have h₁ := congr_fun ((complexBasis α).sum_repr f) a
  simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one, map_zero_eq_one, if_pos rfl,
    if_neg ha, f] at h₀ h₁
  exact one_ne_zero (h₁.symm.trans h₀)

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