Commit 2023-12-20 00:53 b8e33bbb

View on Github →

feat: add ContinuousMap.compStarAlgHom, postcomposition by a StarAlgHom (#8992)

Estimated changes

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

added def ContinuousMap.compStarAlgHom

added theorem ContinuousMap.compStarAlgHom_comp

added theorem ContinuousMap.compStarAlgHom_id