Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces

DOI10.2478/FORMA-2022-0006MaRDI QIDQ6489402

Yuichi Futa, Kazuhisa Nakasho

Publication date: 22 April 2024

Published in: Formalized Mathematics (Search for Journal in Brave)

zbMATH Keywords

Banach spacecomposition functionmultilinear function

Mathematics Subject Classification ID

Multilinear algebra, tensor calculus (15A69) Forms (bilinear, sesquilinear, multilinear) (47A07) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• Isometric differentiable functions on real normed space
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Multilinear operator and its basic properties
• Continuity of Barycentric Coordinates in Euclidean Topological Spaces
• Mizar: State-of-the-art and Beyond

This page was built for publication: Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces