Commit 2023-06-08 03:38 61017237

View on Github →

feat: port Topology.Algebra.Module.CharacterSpace (#4819)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Module/CharacterSpace.lean

added theorem WeakDual.CharacterSpace.apply_mem_spectrum

added theorem WeakDual.CharacterSpace.coe_toClm

added theorem WeakDual.CharacterSpace.coe_toNonUnitalAlgHom

added theorem WeakDual.CharacterSpace.eq_set_map_one_map_mul

added theorem WeakDual.CharacterSpace.ext

added theorem WeakDual.CharacterSpace.ext_ker

added def WeakDual.CharacterSpace.toAlgHom

added def WeakDual.CharacterSpace.toClm

added def WeakDual.CharacterSpace.toNonUnitalAlgHom

added theorem WeakDual.CharacterSpace.union_zero

added theorem WeakDual.CharacterSpace.union_zero_isClosed

added def WeakDual.characterSpace

added def WeakDual.gelfandTransform