Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-30 21:09 14b597c3

View on Github →

feat(analysis/normed_space): ∥n • a∥ ≤ n * ∥a∥ (#7745) From LTE.

Estimated changes

added theorem nnnorm_gsmul_le
added theorem nnnorm_nsmul_le
added theorem norm_gsmul_le
added theorem norm_nsmul_le