stone_weierstrass): generalize the complex Stone-Weierstrass theorem to is_R_or_C fields (#14374)

Commit

3 years ago

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.

Author

dupuisf

Parents

c5b3de8d

mathlib 634bef9f - feat(topology/continuous_function/stone_weierstrass): generalize the complex Stone-Weierstrass theorem to is_R_or_C fields (#14374)

mathlib
634bef9f - feat(topology/continuous_function/stone_weierstrass): generalize the complex Stone-Weierstrass theorem to is_R_or_C fields (#14374)