Mathlib Changelog
Changelog
About
Github
Commit
2021-06-29 17:54
bdf2d81e
View on Github →
feat(topology/continuous_function/stone_weierstrass): complex Stone-Weierstrass (
#8012
)
Estimated changes
Modified
src/analysis/complex/basic.lean
added
theorem
complex.continuous_abs
added
theorem
complex.continuous_norm_sq
Modified
src/topology/algebra/module.lean
added
theorem
submodule.topological_closure_map
added
theorem
submodule.topological_closure_mono
Modified
src/topology/continuous_function/algebra.lean
Modified
src/topology/continuous_function/bounded.lean
added
theorem
continuous_linear_map.comp_left_continuous_bounded_apply
Modified
src/topology/continuous_function/compact.lean
added
theorem
continuous_linear_map.comp_left_continuous_compact_apply
added
theorem
continuous_linear_map.to_linear_comp_left_continuous_compact
added
theorem
continuous_map.linear_isometry_bounded_of_compact_apply_apply
added
theorem
continuous_map.linear_isometry_bounded_of_compact_symm_apply
Modified
src/topology/continuous_function/stone_weierstrass.lean
added
def
continuous_map.conj_invariant_subalgebra
added
theorem
continuous_map.mem_conj_invariant_subalgebra
added
theorem
continuous_map.subalgebra_complex_topological_closure_eq_top_of_separates_points
added
theorem
subalgebra.separates_points.complex_to_real