Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm_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 norm_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 norm_gsmul_leView on Github →