Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 01:25 09a7f7a1

View on Github →

refactor(algebra/algebra/subalgebra/basic): Remove ' from subalgebra.comap' (#15349) This PR removes ' from subalgebra.comap'. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/subalgebra.2Ecomap'

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

modified theorem algebra.comap_top

deleted def subalgebra.comap'

added def subalgebra.comap

modified theorem subalgebra.gc_map_comap

Modified src/topology/algebra/algebra.lean

deleted theorem subalgebra.topological_closure_comap'_homeomorph

added theorem subalgebra.topological_closure_comap_homeomorph

Modified src/topology/continuous_function/polynomial.lean

deleted theorem polynomial_functions.comap'_comp_right_alg_hom_Icc_homeo_I

added theorem polynomial_functions.comap_comp_right_alg_hom_Icc_homeo_I

Modified src/topology/continuous_function/stone_weierstrass.lean

Modified src/topology/continuous_function/weierstrass.lean