Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 17:33 958c407a

View on Github →

chore(analysis/normed_space/basic): a few lemmas about nnnorm (#5532)

Estimated changes

Modified src/analysis/normed_space/basic.lean

modified theorem coe_nnnorm

added theorem mem_emetric_ball_0_iff

added theorem normed_field.nnnorm_div

added theorem normed_field.nnnorm_fpow

added def normed_field.nnnorm_hom

added theorem normed_field.nnnorm_mul

added theorem normed_field.nnnorm_pow

added theorem normed_field.nnnorm_prod