mathlib3

c2258f7b - chore(topology/continuous_function/ideals): generalize type class requirements (#19093)

chore(topology/continuous_function/ideals): generalize type class requirements (#19093) For the continuous functional calculus in non-unital algebras the subtype `C(R, R)₀ := { f : C(R, R) // f 0 = 0 }` will be useful, which is exactly `continuous_map.ideal_of_set`. However, it will be necessary to let `R` be `ℂ`, `ℝ` and `ℝ≥0`, and for the latter we need these more general type class assumptions.