Mathlib v3 is deprecated. Go to Mathlib v4

Theorem coe_homeomorph_unit_ball_apply_zero

Modification history

2022-08-15 09:04
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980) …
Added coe_homeomorph_unit_ball_apply_zeroView on Github →