Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-23 16:03 2e83666b

View on Github →

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

Estimated changes