Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-10 01:51 0a348784

View on Github →

chore(topology/algebra/continuous_functions): making names consistent with the smooth library (#7844)

Estimated changes

added theorem continuous_map.coe_div
added theorem continuous_map.coe_inv
added theorem continuous_map.coe_mul
added theorem continuous_map.coe_one
added theorem continuous_map.coe_pow
deleted theorem continuous_map.div_coe
deleted theorem continuous_map.inv_coe
deleted theorem continuous_map.mul_coe
deleted theorem continuous_map.one_coe
deleted theorem continuous_map.pow_coe
deleted theorem continuous_map.smul_coe