{"entities":{"Q52541":{"pageid":52597,"ns":120,"title":"Item:Q52541","lastrevid":56966313,"modified":"2026-03-25T09:37:03Z","type":"item","id":"Q52541","labels":{"en":{"language":"en","value":"mathlib"}},"descriptions":{"en":{"language":"en","value":"The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant."}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"4f1ef6b06c20f73e455a890e8b9347fcc594e943","datavalue":{"value":"36839","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$18378666-4133-4C4C-8AB8-6BD881BD0DBE","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"8d53fc817fa25c376ea8904337ebf1c838c40b6b","datavalue":{"value":{"entity-type":"item","numeric-id":2219408,"id":"Q2219408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$65AEF066-2BEC-414C-ACD1-5CE3BDF6385D","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":"Q52541$96C1E585-5859-441A-BA72-B3E87EF8D8EC","rank":"normal"}],"P339":[{"mainsnak":{"snaktype":"value","property":"P339","hash":"eadf12c91410b678cf0cb6222548afa0d84dc498","datavalue":{"value":"https://github.com/leanprover-community/mathlib","type":"string"},"datatype":"url"},"type":"statement","id":"Q52541$DAAFD8CE-D431-4FAD-A38B-5AC2775096CD","rank":"normal"}],"P1454":[{"mainsnak":{"snaktype":"value","property":"P1454","hash":"79c7d49d325669f6f2b151c217cab3e058a3dcc4","datavalue":{"value":"swh:1:snp:6ac2bad6d01a136c67b3204cd17f43da668a93ac","type":"string"},"datatype":"external-id"},"type":"statement","qualifiers":{"P339":[{"snaktype":"value","property":"P339","hash":"eadf12c91410b678cf0cb6222548afa0d84dc498","datavalue":{"value":"https://github.com/leanprover-community/mathlib","type":"string"},"datatype":"url"}],"P140":[{"snaktype":"value","property":"P140","hash":"b762e1da0c8d4d3efd756a1187a553421953b66c","datavalue":{"value":{"time":"+2024-03-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"}]},"qualifiers-order":["P339","P140"],"id":"Q52541$E4723EA7-E416-4A74-82A3-3DEF61C83EE0","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"ce23831c38dbef7d8bc930017267df69a1ba38be","datavalue":{"value":"https://leanprover-community.github.io","type":"string"},"datatype":"url"},"type":"statement","id":"Q52541$59E872D3-7791-4258-B47A-072F76BFB45D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$9027139B-0EB6-42F5-A9F1-67EE8116C283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$4553567E-40A3-4F70-B4C5-12F266A896CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8befc1ffe367aef867e4dcd902eb59cbacd3a347","datavalue":{"value":"13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$1065020F-22A7-43B7-8520-3FE515CD028D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$0EE6D4A3-5FDA-46D5-A3CA-162BB30A2C7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$E8B3E04B-F627-4702-8969-13DCAFB7D001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ae9c75c1f07ce06d85b9552d2104619090f82402","datavalue":{"value":"00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$04852D50-C0AC-41AA-A641-097D29C87AC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ccc624529bfb589cae1d19db3eb04dd4b43978c3","datavalue":{"value":"01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$AF07F794-A072-4B43-8F03-A7CA95C16D7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$B4FC413A-FA9B-4BDF-937B-6C1C8D7F7387","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d379e93a1cc3ab3df2a5b8d85c84eb0620f6469c","datavalue":{"value":"06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$3692533B-AAFD-4E07-8409-9A4AF69CEFA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d57514d4788d5abbd1056aadd506bc3f1b86263e","datavalue":{"value":"08","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$3ECCC0BC-7F16-494D-875A-4DE4A860F7E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f5c899803a3ce2dc0dd1263cc65df28aab94054","datavalue":{"value":"12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$5AE05958-0EF1-493A-AC46-E9AB24678E93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd4f0694ac7a00e4fadde328cdb4437f6c066de7","datavalue":{"value":"14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$5BE1464D-8976-4F9B-A131-3FEF262D3322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5dd818343d7a5b259737eac61518c19de74ecd35","datavalue":{"value":"15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$E5F50697-CEC1-45C3-B74A-AAA26F6DC624","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c6cc7c76b3cafafac08dd013fc5ce16db183bb48","datavalue":{"value":"16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$1ED3090C-081F-42AC-A0BF-CBA98CD53A65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6652165beef23109cbf13f7bcea8ff518e7cac51","datavalue":{"value":"17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$16EE8D17-8E43-4D36-B713-8BD3299F2480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c42d8309659ef226cd875765a3c9064bb7558782","datavalue":{"value":"20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$B65BE51A-3C25-48EA-BB4F-C6A946479B69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdcc80d920f5e4d163108380bb0c7de24bca08b4","datavalue":{"value":"26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$E99FA525-AAA6-46FA-ADEC-8B5EC5F19310","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"be5267d4895a58dcc5cf7a7e416f12795fbbed35","datavalue":{"value":"28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$DD95BB50-188F-40A5-AE0D-E07826809AE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca97ab6736a2cf36b4aa3171cbf7b0139773b03d","datavalue":{"value":"46","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$4D8B7F5E-5CFB-43F5-9FAA-C7B5E5A51CD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9c36f543604e3fdf981f5fb6ed78b53d6c52253c","datavalue":{"value":"47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$C7994765-5073-405F-B726-7101F92D6FC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"389057ea232b6d266cab69038163241bd07104b6","datavalue":{"value":"51","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$4CAF8C3E-0719-41F7-A8C8-7158B47FED69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e24ee68b43931de13fa3c2edb783c4c41f7c841b","datavalue":{"value":"55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$23602FCA-37C8-481C-86E8-B20A7B2EEB0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cb0bb3315ea6d324166d2a3b9e8cc481541ca3cc","datavalue":{"value":"57","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$E15671DD-653B-4402-92BC-0A959D0CAC42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$559D62E3-0E63-414E-84F8-0D1FB506BE53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4edc7e695c3667a3dc24594c0516548b87f81467","datavalue":{"value":"81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$119872CB-38A0-4B33-84C6-1525693BDA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8765ff2acd582c5d837fde50b2a0cf51b0c3e2a2","datavalue":{"value":"82","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$27FB80E8-F363-4236-B958-035D8D07EF58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$363985DE-0F31-447D-ACD2-583D9FF9DC16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q52541$4C5A238D-128D-40D6-A7E7-1CB58CD237E0","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7434bcf5c727d2c07e931aea1694436d0b39cd53","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$22B17FCC-E003-447F-935B-EFD823DF7557","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$D8592838-06F3-4AF5-9DDC-317F368BA136","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":"Q52541$0EA4E3CC-830F-48DF-BC44-FAD557345E74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$2A0D873C-28A0-4C63-A6CD-406D7FDE1F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ec62e09023b4499a5f32d5b66aa8722181c9532c","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$CFCB62E9-2998-4061-A764-5C8A57BAAFC5","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":"Q52541$2DF03E9F-DD57-4C77-B409-A5389C5D1149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2ded5a481ece08049848bd1edb3f9afa21f0df2f","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$433EC37F-C239-467B-B4C9-C308493A9753","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":"Q52541$673572A0-B1ED-454B-A5D5-B2A13B2C0130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cea2a7e9bb130921d12e1d361b3d4585036772c9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$5699B992-5CEA-47AB-AA52-D41FFA45F928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b28c81d4911883bef3214e7956987a08537ccfe0","datavalue":{"value":{"entity-type":"item","numeric-id":27033,"id":"Q27033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$52A0697F-22CD-4542-818F-642B8B1CD4AF","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":"Q52541$871ADCFE-B047-4E8B-8C8A-106AF793FEF2","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":"Q52541$3E1922D3-1590-493F-AABB-F036B586E563","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9e7a1624ebcfc86cb11ccad80d0985ed6ed992b9","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$EF8D4F8B-B4E7-46F9-9522-D457EADD0A26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"255d1eab6148b0a0149f5ba251f819f772375a4c","datavalue":{"value":{"entity-type":"item","numeric-id":23492,"id":"Q23492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$6B82F2DF-3E49-4852-8164-7F03F1728BAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"053ea061eb2db1c9b7f27b25da993bb19055407c","datavalue":{"value":{"entity-type":"item","numeric-id":25224,"id":"Q25224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q52541$0E4C1879-EC3B-4CAE-A0AA-F203042014C5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mathlib","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mathlib"}}}}}