Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-23 17:07 ef901ea6

View on Github →

refactor(*): rename nondiscrete_normed_field (#15625) This renames nondiscrete_normed_field to nontrivially_normed_field in accordance with this Zulip discussion

Estimated changes

modified theorem diff_cont_on_cl.smul
modified theorem diff_cont_on_cl.smul_const
modified structure implicit_function_data
modified def normed_space.polar
modified theorem ext_chart_model_space_eq_id
modified structure model_with_corners