{"entities":{"Q7361019":{"pageid":31518596,"ns":120,"title":"Item:Q7361019","lastrevid":105362420,"modified":"2026-10-07T13:34:12Z","type":"item","id":"Q7361019","labels":{"en":{"language":"en","value":"Vector Spaces"}},"descriptions":{"en":{"language":"en","value":"AFP entry VectorSpace"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9cce04f098874eb2ded9b56bde15c0ceb88c4a62","datavalue":{"value":"https://isa-afp.org/entries/VectorSpace.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361019$992095E2-7B2D-40E0-ADA5-0960C7A67C0A","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":"Q7361019$4BCA490A-9012-46D0-9EE0-0A8F5F49A5A9","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a286713eefbd53d281740bbd928acf0f96ba73a9","datavalue":{"value":"Holden Lee","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361019$4A3B1234-4DFE-4F37-93C2-B6EBE2EFA214","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"31e2a6f480d07fe6bb6a42c8010259994f530e06","datavalue":{"value":{"text":"Vector Spaces","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361019$DDF35431-AA0A-4E48-8577-DB7C039740BF","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":"Q7361019$7C7B1C3C-CC0D-416D-8B1F-150B645A258B","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":"Q7361019$053EAA83-1557-40F4-B48D-714E6A38CB41","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":"Q7361019$24217994-6973-43DD-AAE0-6055F4BBDBE9","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":"Q7361019$2003ECA0-3573-4CCB-A989-03C690C98269","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Vector Spaces (AFP entry VectorSpace)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Vector_Spaces_(AFP_entry_VectorSpace)"}}}}}