Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 13:27 5254ef14

View on Github →

feat(topology/continuous_function): lemmas about coe (#7055)

Estimated changes

Modified src/topology/continuous_function/algebra.lean

added def coe_fn_monoid_hom

added theorem continuous_map.coe_prod

added theorem continuous_map.prod_apply