Theorems · Theorem · functional analysis

WeakDual.CharacterSpace.exists_apply_eq_zero

∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] {a : A},
  ¬IsUnit a → ∃ f, f a = 0

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.

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandDuality

Cited by

1 results in Mathlib

Foundations

Depth 300 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedCommRingNormedAlgebraCompleteSpace