Commit 2023-06-11 20:55 95092b27

View on Github →

feat: port Analysis.NormedSpace.Star.GelfandDuality (#4972)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

added theorem Ideal.toCharacterSpace_apply_eq_zero_of_mem

added theorem WeakDual.CharacterSpace.compContinuousMap_comp

added theorem WeakDual.CharacterSpace.compContinuousMap_id

added theorem WeakDual.CharacterSpace.exists_apply_eq_zero

added theorem WeakDual.CharacterSpace.mem_spectrum_iff_exists

added theorem gelfandTransform_bijective

added theorem gelfandTransform_isometry

added theorem gelfandTransform_map_star

added theorem spectrum.gelfandTransform_eq