Def ContinuousMap.compStarAlgHom

Modification history

2024-11-04 13:07

Mathlib/Topology/ContinuousMap/Algebra.lean

chore: split Topology/ContinuousMap/Algebra (#18604) …

Modified ContinuousMap.compStarAlgHom View on Github →

2023-12-20 00:53

Mathlib/Topology/ContinuousFunction/Algebra.lean

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

Added ContinuousMap.compStarAlgHom View on Github →