Theorem ContinuousMapZero.adjoin_id_dense

Modification history

2025-09-18 15:32
Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
refactor: switch to using `Fact (0 ∈ s)` for `ContinuousMapZero.id` (#29563) …
Modified ContinuousMapZero.adjoin_id_denseView on Github →
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 ContinuousMapZero.adjoin_id_denseView on Github →