{"entities":{"Q40376":{"pageid":40432,"ns":120,"title":"Item:Q40376","lastrevid":105426344,"modified":"2026-10-09T10:05:12Z","type":"item","id":"Q40376","labels":{"en":{"language":"en","value":"Vector Spaces"}},"descriptions":{"en":{"language":"en","value":"AFP entry VectorSpace"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"5c4bf006c0eb292554ece248ad6eff9e33556632","datavalue":{"value":"28662","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$BC5309AC-5576-4941-9473-6FFE031CE52C","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$BAE06A59-977F-44BC-B73A-C443AC340A0B","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"d11dadd092d24324b0a57ba411aa26191abd4627","datavalue":{"value":"https://www.isa-afp.org/entries/VectorSpace.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40376$CDC66250-996C-4DB2-8603-21EAD9ED7955","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$138E841E-7CC7-4A71-A213-E7A08B24FF50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$43DEE09B-B403-4B6E-BB4E-90A28C84F7A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f5c899803a3ce2dc0dd1263cc65df28aab94054","datavalue":{"value":"12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$53B1656B-1DF2-4003-A73A-E5957DA83C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8befc1ffe367aef867e4dcd902eb59cbacd3a347","datavalue":{"value":"13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$E611F907-3B55-4EA5-9C9C-B9E1C0912EF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$0C9540D5-2E62-4C94-B59E-A8F0D895C47C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$835B3BFB-D617-488F-9A9D-8E3A199CF053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd53baf500a6931877eb74cf8c39e6d35302628a","datavalue":{"value":"11.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$94B4B89A-3308-4A33-ABC6-A0E877EB69BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2230d337deb7b90f21aa1a2ec63051e97d36fcd5","datavalue":{"value":"12.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$86C09063-5D33-4477-A821-3CBE1EAFC1A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62b7e192ddad84e0999f497c95811da22d169570","datavalue":{"value":"13.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$396D0B9C-2077-4E8D-A930-F23FC922B8CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40376$ACE9AC35-865D-41FE-9851-AE53C2AEF6A7","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7d1a8519018039436924ad678b461ed447b5bd71","datavalue":{"value":{"entity-type":"item","numeric-id":40310,"id":"Q40310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$0A829954-8D6F-407A-85E0-B379F6E25E21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$263895B9-B481-409F-A30F-6B9802C82024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$A765BDAD-61E1-445C-A3CC-DB696B26511B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ed15eb8701a335444fde1bcc3327d1067ce64751","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$B6A38A29-6CDC-4649-ABFE-1F24C29B6B36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$93D5CC17-B2A2-4970-BBA1-05B498CF45DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$EA1035D4-D139-4A80-9B8B-5B96544E4BE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7743e545277c1ef055fd43ece5fc5f10932fd356","datavalue":{"value":{"entity-type":"item","numeric-id":43916,"id":"Q43916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$022D5F0E-A9B2-4DB2-8983-42E2EA67ED11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9eb436930ab1f6d235b354c651322b547341064b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$BA039922-DABA-4A9F-9C0A-A9B69DD5C6EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0f29c9b1edecb5ae8b8679151a51782e90d9480e","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$70CA9B2B-4617-4320-AE45-BF5213A4A67D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c7cf914fa2ed02c8c123a4c265842a9ab4be0800","datavalue":{"value":{"entity-type":"item","numeric-id":25403,"id":"Q25403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$7C90CB81-28ED-48A9-8FF6-7C93AD14D954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"83a7c52533a2a0c00f328cde038f2bdb12749a41","datavalue":{"value":{"entity-type":"item","numeric-id":40375,"id":"Q40375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$2DA7A647-7C5F-4A9B-912C-4891C52FF7FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b05ebaa65438167fd8c160361611fffcc4886639","datavalue":{"value":{"entity-type":"item","numeric-id":40374,"id":"Q40374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$D4F8341A-A025-4753-A733-34047657B9A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82152c1528c5be7e2040d1abd74977f4fe51817","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$58421695-0AAC-44F8-8A98-B1AACF9C4E71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$14973AD0-2C8C-4401-BC28-066F61F1FCF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$CA18DDBD-5080-4239-8F06-16F91F104C4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4dfac822d106dc7f697754008c4906d0b5156921","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$6E98B138-AAE0-4A9E-A57D-C80BA2E1918E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9cce04f098874eb2ded9b56bde15c0ceb88c4a62","datavalue":{"value":"https://isa-afp.org/entries/VectorSpace.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40376$F053E74F-B7C3-4138-B399-AC22B4647A93","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a286713eefbd53d281740bbd928acf0f96ba73a9","datavalue":{"value":"Holden Lee","type":"string"},"datatype":"string"},"type":"statement","id":"Q40376$16F6AD84-AE19-4995-9FE5-1B11FFDA6FB0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3bc400b0e35a8f7c57fafcaf182e9a957dd3a71f","datavalue":{"value":"This formalisation of basic linear algebra is based completely on locales, building off HOL-Algebra. It includes basic definitions: linear combinations, span, linear independence; linear transformations; interpretation of function spaces as vector spaces; the direct sum of vector spaces, sum of subspaces; the replacement theorem; existence of bases in finite-dimensional; vector spaces, definition of dimension; the rank-nullity theorem. Some concepts are actually defined and proved for modules as they also apply there. Infinite-dimensional vector spaces are supported, but dimension is only supported for finite-dimensional vector spaces. The proofs are standard; the proofs of the replacement theorem and rank-nullity theorem roughly follow the presentation in Linear Algebra by Friedberg, Insel, and Spence. The rank-nullity theorem generalises the existing development in the Archive of Formal Proof (originally using type classes, now using a mix of type classes and locales).","type":"string"},"datatype":"string"},"type":"statement","id":"Q40376$60DDCD94-0424-4A2D-BA39-76DE3EE7B340","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"163bad71d2d58b992a56c87b8eddb84d83e1a225","datavalue":{"value":{"time":"+2014-08-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40376$B8144ACC-239D-48C1-8097-82EFBD95417C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"31e2a6f480d07fe6bb6a42c8010259994f530e06","datavalue":{"value":{"text":"Vector Spaces","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40376$2B4952CB-949D-41FB-B69D-5FC0500B4F4F","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$AD564675-117B-4176-8EF2-3F76A496C0B2","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65292b3c42fa1bd5c21e4c91fe94fdc3f630f232","datavalue":{"value":{"entity-type":"item","numeric-id":7360821,"id":"Q7360821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40376$E0F6078B-D4B9-48FF-AD7E-B8A9D388FAE0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Vector Spaces","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Vector_Spaces"}}}}}