English
If a is not a unit in a NormedCommRing A, there exists a character f in the complex character space such that f(a) = 0.
Русский
Если a не является единицей в нормированной коммутативной банаховой алгебре A, существует характер f из комплексного пространства характеристик, такой что f(a) = 0.
LaTeX
$$$$\exists f \in \text{characterSpace} \; \mathbb{C} \; (f(a) = 0)$$$$
Lean4
/-- If `a : A` is not a unit, then some character takes the value zero at `a`. This is equivalent
to `gelfandTransform ℂ A a` takes the value zero at some character. -/
theorem exists_apply_eq_zero {a : A} (ha : ¬IsUnit a) : ∃ f : characterSpace ℂ A, f a = 0 :=
by
obtain ⟨M, hM, haM⟩ := (span { a }).exists_le_maximal (span_singleton_ne_top ha)
exact
⟨M.toCharacterSpace, M.toCharacterSpace_apply_eq_zero_of_mem (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩
