Mathlib Changelog
v4
Changelog
About
Github
Theorem
MultilinearMap.norm_map_coord_zero
Modification history
2024-11-28 16:12
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
chore(Analysis/Multilinear): avoid explicit `variable`s (#19445) …
Modified
MultilinearMap.norm_map_coord_zero
View 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_zero
View on Github →