Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnnorm_gsmul_le

Modification history

2021-10-28 02:37
src/analysis/normed_space/basic.lean
chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010) …
Deleted nnnorm_gsmul_leView on Github →
2021-06-23 17:29
src/analysis/normed_space/basic.lean
feat(analysis/normed_space/basic): add has_nnnorm (#7986) …
Modified nnnorm_gsmul_leView on Github →
2021-05-30 21:09
src/analysis/normed_space/basic.lean
feat(analysis/normed_space): ∥n • a∥ ≤ n * ∥a∥ (#7745) …
Added nnnorm_gsmul_leView on Github →