Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-31 09:30 1fdce2f8

View on Github →

refactor(analysis/normed_space/basic): add semi_normed_ring (#6889) This is the natural continuation of #6888 . We add here semi_normed_ring, semi_normed_comm_ring, semi_normed_space and semi_normed_algebra. I didn't add semi_normed_field: the most important result for normed_field is ∥1∥ = 1, that is false for semi_normed_field, making it a more or less useless notion. In particular a semi_normed_space is by definition a vector space over a normed_field.

Estimated changes

modified theorem closure_ball
modified theorem dist_smul
modified theorem frontier_ball
modified theorem frontier_closed_ball
modified theorem interior_closed_ball
modified theorem nndist_smul
modified theorem nnnorm_norm
modified theorem nnnorm_one
modified theorem nnnorm_smul
modified theorem norm_algebra_map_eq
modified theorem norm_norm
modified theorem norm_smul
modified theorem norm_smul_of_nonneg
modified theorem normed_group.tendsto_at_top