Mathlib Changelog
v4
Changelog
About
Github
Def
ContinuousAlternatingMap.toContinuousMultilinearMapCLM
Modification history
2025-05-17 18:54
Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
feat(Analysis/NormedSpace): add `NormedSpace.Alternating` (#8691) …
Added
ContinuousAlternatingMap.toContinuousMultilinearMapCLM
View on Github →