Theorem ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom

Modification history

2024-05-29 16:56
Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean
feat: the non-unital star subalgebra generated by `id` is dense in `C(s, 𝕜)₀` (#13326) …
Added ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHomView on Github →