mathlib
14b597c3 - feat(analysis/normed_space): ∥n • a∥ ≤ n * ∥a∥ (#7745)

Commit

4 years ago

feat(analysis/normed_space): ∥n • a∥ ≤ n * ∥a∥ (#7745) From LTE. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents