algebra): functoriality of `C(⬝, A)` into star algebras. (#16817)

Commit

3 years ago

feat(topology/continuous_function/algebra): functoriality of `C(⬝, A)` into star algebras. (#16817) This is one of the two functors involved in Gelfand duality.

Author

j-loreaux

Parents

083202d6

mathlib3 2e83666b - feat(topology/continuous_function/algebra): functoriality of `C(⬝, A)` into star algebras. (#16817)

mathlib3
2e83666b - feat(topology/continuous_function/algebra): functoriality of `C(⬝, A)` into star algebras. (#16817)