Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-21 11:05 5d67033c

View on Github →

feat(topology/algebra/continuous_functions): missing lemmas (#6782)

Estimated changes

Modified src/topology/algebra/continuous_functions.lean

added theorem algebra_map_apply

added theorem continuous_map.C_apply

added theorem continuous_map.div_comp

added theorem continuous_map.inv_comp

added theorem continuous_map.mul_comp

added theorem continuous_map.pow_comp

added theorem continuous_map.smul_comp

added theorem inv_coe

added theorem pow_coe