Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-29 10:59 a5a7a753

View on Github →

feat(analysis/normed_space): define normed_comm_ring (#4291) Also use section variables.

Estimated changes

modified theorem ring_hom.map_fpow
added theorem monoid_hom.map_fpow
modified theorem normed_field.exists_lt_norm
modified theorem normed_field.exists_norm_lt
modified theorem normed_field.nnnorm_inv
modified theorem normed_field.nnnorm_one
modified theorem normed_field.norm_div
modified theorem normed_field.norm_fpow
modified theorem normed_field.norm_inv
modified theorem normed_field.norm_mul
modified theorem normed_field.norm_one
modified theorem normed_field.norm_pow
modified theorem normed_field.norm_prod
modified theorem normed_field.tendsto_inv