Theorem MultilinearMap.norm_map_coord_zero

Modification history

2026-10-29 21:19
Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …
Modified MultilinearMap.norm_map_coord_zeroView on Github →
2024-11-28 16:12
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
chore(Analysis/Multilinear): avoid explicit `variable`s (#19445) …
Modified MultilinearMap.norm_map_coord_zeroView on Github →
2024-01-20 11:07
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
feat(Analysis/NormedSpace/Multilinear.Basic): operator norm on `ContinuousMultilinearMap` for seminormed spaces (#9700) …
Added MultilinearMap.norm_map_coord_zeroView on Github →