Commit 2024-09-11 00:28 a8f1816e

View on Github →

feat: star monomorphisms between C⋆-algebras are isometric (#16599)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Unitization.lean

added def Unitization.starMap

added theorem Unitization.starMap_comp

added theorem Unitization.starMap_id

added theorem Unitization.starMap_injective

added theorem Unitization.starMap_inl

added theorem Unitization.starMap_inr

added theorem Unitization.starMap_surjective

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

Created Mathlib/Analysis/CStarAlgebra/Hom.lean

added theorem IsSelfAdjoint.map_spectrum_real

added theorem NonUnitalStarAlgHom.isometry

added theorem NonUnitalStarAlgHom.nnnorm_map

added theorem NonUnitalStarAlgHom.norm_map