Commit 2022-05-26 02:20 634bef9f

View on Github →

feat(topology/continuous_function/stone_weierstrass): generalize the complex Stone-Weierstrass theorem to is_R_or_C fields (#14374) This PR generalizes the complex Stone-Weierstrass theorem to hold for an is_R_or_C field.

Estimated changes

Modified src/analysis/fourier.lean

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.continuous_abs

added theorem is_R_or_C.continuous_norm_sq

Modified src/topology/continuous_function/stone_weierstrass.lean

modified def continuous_map.conj_invariant_subalgebra

modified theorem continuous_map.mem_conj_invariant_subalgebra

deleted theorem continuous_map.subalgebra_complex_topological_closure_eq_top_of_separates_points

added theorem continuous_map.subalgebra_is_R_or_C_topological_closure_eq_top_of_separates_points

deleted theorem subalgebra.separates_points.complex_to_real

added theorem subalgebra.separates_points.is_R_or_C_to_real