Commit 2024-05-29 14:23 593d80d9

View on Github →

feat: add more features to ContinuousMapZero (#13323) This adds all the remaining material necessary for ContinuousMapZero to get the instances of the non-unital continuous functional calculus.

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/ContinuousMapZero.lean

added theorem ContinuousMapZero.coe_neg

added theorem ContinuousMapZero.coe_toContinuousMapHom

modified theorem ContinuousMapZero.embedding_toContinuousMap

added def ContinuousMapZero.nonUnitalStarAlgHom_postcomp

added def ContinuousMapZero.nonUnitalStarAlgHom_precomp

modified theorem ContinuousMapZero.range_toContinuousMap

added def ContinuousMapZero.toContinuousMapHom

added theorem ContinuousMapZero.toContinuousMap_id

modified theorem ContinuousMapZero.toContinuousMap_injective

added theorem ContinuousMapZero.uniformEmbedding_comp

added def UniformEquiv.arrowCongrLeft₀