{"entities":{"Q6867741":{"pageid":20703043,"ns":120,"title":"Item:Q6867741","lastrevid":104144042,"modified":"2026-06-09T10:56:41Z","type":"item","id":"Q6867741","labels":{"en":{"language":"en","value":"Formalization of derived categories in Lean/mathlib"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8151345"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$1FC646E2-0F03-458C-8C7B-A7F1AC7BC386","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2eec32cd04da880c2b92b7a80c096ef1eecd67ae","datavalue":{"value":{"text":"Formalization of derived categories in Lean/mathlib","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6867741$91221430-D4D7-4E42-AEE8-B460147884DD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"17ac4013c0de14860c4c2d8a5bae80f8690f5dc9","datavalue":{"value":"10.46298/AFM.13609","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$02BA480D-18B5-4CB6-B1CF-9FB1870E6D9E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"666568ec2e61d240112176f39cffde236d9d0dbd","datavalue":{"value":{"entity-type":"item","numeric-id":866581,"id":"Q866581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$9B9F6B70-8C78-4A14-B3A4-0DB287812A50","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ffaa058198f7b067fc51d35b10c4ebc3a0824454","datavalue":{"value":{"entity-type":"item","numeric-id":6867736,"id":"Q6867736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$896A61A2-D569-46B9-B3D7-0A571174ED5D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b21df698a706abcc2fd283bd51480ce9f9a58001","datavalue":{"value":{"time":"+2026-01-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6867741$E9F5B3D2-65E4-4855-A551-0C2C40CD5478","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$F7CD55AF-5A67-497B-8509-966C74375CC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec042405e978dbe591fcb4494676c8e9f7034623","datavalue":{"value":"18G80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$4E8857A3-1D23-4520-BD1A-D6B537FEFD34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"60572561c94bb0a5de4329d3c7bf8a47080901dd","datavalue":{"value":"18G15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$CAE264C4-3C2D-4DAD-82E4-659F48B0A763","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3476e1414024b63d1891ee4733ade3e7579c02ec","datavalue":{"value":"18G40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$B9A15504-204F-40DF-99D4-7693DCBF4E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9a626f2bdfa0328af9d23fb451b774749f3536d8","datavalue":{"value":"18E35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$0781235E-CFE3-40E4-9069-A029D7EDA221","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"abd2418888491158a03dc163afa335072c7a7d14","datavalue":{"value":"8151345","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6867741$9AEC0E4F-757B-4C08-9998-D2F04FFA5CCE","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$82CC8F7B-1B9E-425D-B25A-4A33AAB68ADD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00c54ac78bf5553f64b9cd583f9b2aa460638484","datavalue":{"value":"derived category","type":"string"},"datatype":"string"},"type":"statement","id":"Q6867741$B832346B-E622-4616-8BC2-C547D2BB6244","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e85250b0f5793fddfbfacbacf1a198f152b6c2ef","datavalue":{"value":"homological algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q6867741$B374F1E2-9FE2-401B-BBA2-327A360A6730","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d649b5d4a84919b7669ba1ad53c37a6dfb8e0baf","datavalue":{"value":"spectral sequence","type":"string"},"datatype":"string"},"type":"statement","id":"Q6867741$27F7D274-9D2F-496C-9554-2C430B42DFD3","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$07E90E5E-7766-463F-A159-4247775AEE16","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"af5454750f5d297118e2d43ae886b47301283891","datavalue":{"value":{"entity-type":"item","numeric-id":928666,"id":"Q928666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$C4690E43-5E88-4B31-B936-F03E0586534A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85fba442991ce33d00d955cd91376c05e44f258b","datavalue":{"value":{"entity-type":"item","numeric-id":4640173,"id":"Q4640173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$5FDEE702-32EF-4EA1-9CBA-10A163EB02FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65eeabb99db53adaf7c57c5e6c3606fed1fecd86","datavalue":{"value":{"entity-type":"item","numeric-id":4314472,"id":"Q4314472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$6E46F15C-0286-4124-9551-A580C3395E7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a42a19d0fc21ec6f04d8156c3cf07b594f9f5ae","datavalue":{"value":{"entity-type":"item","numeric-id":5094471,"id":"Q5094471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$47A95CB9-983D-415A-8043-F18F72E98CF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3298491323a08b42929ec01173fc3f9b2ca83e9","datavalue":{"value":{"entity-type":"item","numeric-id":4935949,"id":"Q4935949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$F3CA7FEC-7210-4487-ABDF-AE49F572D174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bee365c9ba699c10dec30af783782d8de9d40b8","datavalue":{"value":{"entity-type":"item","numeric-id":1589916,"id":"Q1589916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$120F2D87-9115-436D-B9F8-366FC65BCF51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ce4c18730dab98ffd4f5e9d3ebc25da6bca6d5f","datavalue":{"value":{"entity-type":"item","numeric-id":2528089,"id":"Q2528089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$99427509-FEE8-49AF-A034-8533E16C02CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ff80eff530c98b4d8db99fcd347bf6569d0d014","datavalue":{"value":{"entity-type":"item","numeric-id":2402234,"id":"Q2402234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$ACC96A98-50E0-494B-8287-082A7C5F8269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03afdf275ccfd5f11cb597005a9be741183e0c58","datavalue":{"value":{"entity-type":"item","numeric-id":5580926,"id":"Q5580926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$C90474C7-A208-44C0-9767-0FB5079D6182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"282bcd6e2ec80d6ab53bab0aee042169c5112e43","datavalue":{"value":{"entity-type":"item","numeric-id":6875009,"id":"Q6875009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$CFFBF4AA-DE88-4780-9207-FEF0085100C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f391cbd3c45def2f2ab5b35870ddad1957c24017","datavalue":{"value":{"entity-type":"item","numeric-id":2544562,"id":"Q2544562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$9FB34E6A-D2EE-4C9D-AB47-285B5CC66022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce8eb34d22d0a1dee22aa8d7f83663da2644812a","datavalue":{"value":{"entity-type":"item","numeric-id":2706619,"id":"Q2706619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$646EBB72-6F67-4A60-8479-1FAE4BA3DE7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2791a2a4210bd9f51988e2297ace615165b8c56d","datavalue":{"value":{"entity-type":"item","numeric-id":2639835,"id":"Q2639835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$BD00084A-4251-4E33-8A1D-6D8B8D1BB920","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"711e403c5123478dabe15ec25f8b17fa5a349b38","datavalue":{"value":{"entity-type":"item","numeric-id":927685,"id":"Q927685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$A263E74C-34F3-405F-A6D7-E9D33B6BFBE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e20a61c4525488117caafcb2ffab6b5f8667ad79","datavalue":{"value":{"entity-type":"item","numeric-id":6643004,"id":"Q6643004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$67EFA4B5-A2B7-49E0-8785-616102658958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc5f8bcd9e04d3a3cbbfd22d7a1486b0495087d6","datavalue":{"value":{"entity-type":"item","numeric-id":2650620,"id":"Q2650620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$ABCDBB55-ADF0-47C5-9E17-54D7D4E7B14B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6e65e4b1c1ad9dd4b73248232bf78661ebb9761","datavalue":{"value":{"entity-type":"item","numeric-id":5737117,"id":"Q5737117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$8DF176C3-8E77-4B12-81E8-ABEF26F1E5B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"432347ebf7758fa5347be4c601bf2d08f68cb652","datavalue":{"value":{"entity-type":"item","numeric-id":2055901,"id":"Q2055901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$1F76B5E0-4934-40E9-8E93-5ED731B36D84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"425345705f1aae73238e34997eda6713e637aff6","datavalue":{"value":{"entity-type":"item","numeric-id":2704786,"id":"Q2704786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$290199E8-561E-4005-9536-4EA3217623A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a79fad678f967c6528bd2993b5707c57ab0cbd1","datavalue":{"value":{"entity-type":"item","numeric-id":2530658,"id":"Q2530658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$136193A7-407D-4801-A640-96946D627B3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5abcf41fea649615601f486008c895807c31c664","datavalue":{"value":{"entity-type":"item","numeric-id":2649877,"id":"Q2649877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$7A7AE91F-11FB-4426-8117-5D1EE060B2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d4ac09629ebd61cd24c766d7995c0da0ffd6762","datavalue":{"value":{"entity-type":"item","numeric-id":861700,"id":"Q861700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$2DEB62E1-5418-445B-B50B-0D179CC02FED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85ddb7627231d243e4d801ccf831ba4aa5208f69","datavalue":{"value":{"entity-type":"item","numeric-id":3775700,"id":"Q3775700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$9FF49DDF-B4F3-4946-BE25-F5F2FF0C5380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85b4f89edb7ad5fdc81c4a84f4d2edbb6b808fbd","datavalue":{"value":{"entity-type":"item","numeric-id":4321743,"id":"Q4321743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$BE8823A9-9FE0-4CCE-BCC1-505BF56970BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"24ae15e0e6e096ffff2285b5bed28c0d6cd0974c","datavalue":{"value":{"entity-type":"item","numeric-id":5654808,"id":"Q5654808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$D4527956-F6CB-429C-8DE3-6181F7C152A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a639533052bd954294b314fcbd7d1213f2757aa8","datavalue":{"value":{"entity-type":"item","numeric-id":4193642,"id":"Q4193642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$C5879CB9-3A02-4905-A678-170C8D972623","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bdfcca80cdfe4eb8ca5e9714820eab9e97d8baa","datavalue":{"value":{"entity-type":"item","numeric-id":4342453,"id":"Q4342453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$DB9439BC-198F-49F4-96D6-F52CD26349BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d22a6cda6aca72525e9b325a76d0c7421b4ac4b","datavalue":{"value":{"entity-type":"item","numeric-id":6159373,"id":"Q6159373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$E28780E6-5A45-41BB-A721-86775090A7BA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d863ecadb58c4f267caae253d0bfb45aa139a431","datavalue":{"value":{"entity-type":"item","numeric-id":7257641,"id":"Q7257641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6867741$05438011-4d8a-ff03-17f6-b884e04b3b03","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of derived categories in Lean/mathlib","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_derived_categories_in_Lean/mathlib"}}}}}