{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T02:06:18Z","timestamp":1783908378044,"version":"3.55.0"},"reference-count":11,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    This paper formalizes in Mizar [1], [2], that the isometric isomorphisms between spaces formed by an (\n                    <jats:italic>n<\/jats:italic>\n                    + 1)-dimensional multilinear map and an\n                    <jats:italic>n<\/jats:italic>\n                    -fold composition of linear maps on real normed spaces. This result is used to describe the space of nth-order derivatives of the Frechet derivative as a multilinear space. In Section 1, we discuss the spaces of 1-dimensional multilinear maps and 0-fold compositions as a preparation, and in Section 2, we extend the discussion to the spaces of (\n                    <jats:italic>n<\/jats:italic>\n                    + 1)-dimensional multilinear map and an\n                    <jats:italic>n<\/jats:italic>\n                    -fold compositions. We referred to [4], [11], [8], [9] in this formalization.\n                  <\/jats:p>","DOI":"10.2478\/forma-2022-0006","type":"journal-article","created":{"date-parts":[[2022,12,21]],"date-time":"2022-12-21T05:16:07Z","timestamp":1671599767000},"page":"67-77","source":"Crossref","is-referenced-by-count":1,"title":["Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces"],"prefix":"10.2478","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1110-4342","authenticated-orcid":false,"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Yamaguchi University , Yamaguchi , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuichi","family":"Futa","sequence":"additional","affiliation":[{"name":"Tokyo University of Technology , Tokyo , Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2022,12,21]]},"reference":[{"key":"2026071212490862766_j_forma-2022-0006_ref_001","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-817.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071212490862766_j_forma-2022-0006_ref_002","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071212490862766_j_forma-2022-0006_ref_003","doi-asserted-by":"crossref","unstructured":"[3] Yuichi Futa, Noboru Endou, and Yasunari Shidama. Isometric di erentiable functions on real normed space. Formalized Mathematics, 21(4):249\u2013260, 2013. doi:10.2478\/forma-2013-0027.","DOI":"10.2478\/forma-2013-0027"},{"key":"2026071212490862766_j_forma-2022-0006_ref_004","unstructured":"[4] Miyadera Isao. Functional Analysis. Riko-Gaku-Sya, 1972."},{"key":"2026071212490862766_j_forma-2022-0006_ref_005","doi-asserted-by":"crossref","unstructured":"[5] Kazuhisa Nakasho. Multilinear operator and its basic properties. Formalized Mathematics, 27(1):35\u201345, 2019. doi:10.2478\/forma-2019-0004.","DOI":"10.2478\/forma-2019-0004"},{"key":"2026071212490862766_j_forma-2022-0006_ref_006","doi-asserted-by":"crossref","unstructured":"[6] Karol P\u0105k. Continuity of barycentric coordinates in Euclidean topological spaces. Formalized Mathematics, 19(3):139\u2013144, 2011. doi:10.2478\/v10037-011-0022-5.","DOI":"10.2478\/v10037-011-0022-5"},{"key":"2026071212490862766_j_forma-2022-0006_ref_007","doi-asserted-by":"crossref","unstructured":"[7] Marco Riccardi. Pocklington\u2019s theorem and Bertrand\u2019s postulate. Formalized Mathematics, 14(2):47\u201352, 2006. doi:10.2478\/v10037-006-0007-y.","DOI":"10.2478\/v10037-006-0007-y"},{"key":"2026071212490862766_j_forma-2022-0006_ref_008","unstructured":"[8] Laurent Schwartz. Th\u00e9orie des ensembles et topologie, tome 1. Analyse. Hermann, 1997."},{"key":"2026071212490862766_j_forma-2022-0006_ref_009","unstructured":"[9] Laurent Schwartz. Calcul diff\u00e9rentiel, tome 2. Analyse. Hermann, 1997."},{"key":"2026071212490862766_j_forma-2022-0006_ref_010","unstructured":"[10] Yasunari Shidama. The Banach algebra of bounded linear operators. Formalized Mathematics, 12(2):103\u2013108, 2004."},{"key":"2026071212490862766_j_forma-2022-0006_ref_011","unstructured":"[11] K\u00f4saku Yosida. Functional Analysis. Springer, 1980."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2022-0006","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T01:14:07Z","timestamp":1783905247000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2022-0006"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":11,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,12,21]]},"published-print":{"date-parts":[[2022,4,1]]}},"alternative-id":["10.2478\/forma-2022-0006"],"URL":"https:\/\/doi.org\/10.2478\/forma-2022-0006","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]}}}