{"entities":{"Q438546":{"pageid":440313,"ns":120,"title":"Item:Q438546","lastrevid":61924509,"modified":"2026-04-11T02:35:13Z","type":"item","id":"Q438546","labels":{"en":{"language":"en","value":"A certified proof of the Cartan fixed point theorems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062052"}},"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":"Q438546$19772F59-CAE7-41AB-8121-C46BDF28330F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e9b5dcd32ee280a9004249c5db95c81a42cca4cf","datavalue":{"value":{"text":"A certified proof of the Cartan fixed point theorems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438546$4733B4E2-E83B-4DE2-9F5E-BE56A6226108","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"68ce3796a92f438f92696400717ffbbf30b6d961","datavalue":{"value":"1250.68233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$5CDC8227-900E-43EC-B1C4-7ACF200B6ED1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"96992a7d26938f6aa08a5c9d4f1845441fc21d0a","datavalue":{"value":{"entity-type":"item","numeric-id":438544,"id":"Q438544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$3CAEA20B-CD1E-4502-BDB9-F6EF2F329338","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d6def2eddf42dbd9578c29e8f3dbb54050c87e1","datavalue":{"value":{"entity-type":"item","numeric-id":387722,"id":"Q387722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$8AF2A5BE-F93E-40E4-9DEE-7B5C321E8418","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ea229d5c7d566db264a7e69175c2b14cf582fccb","datavalue":{"value":{"entity-type":"item","numeric-id":438545,"id":"Q438545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$20A53362-89ED-445F-B091-126852FEF84E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$633A9C94-5B46-4E2F-BB83-D88FF855E002","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438546$2978CF1D-5E70-4335-9289-18A61C3DB9DC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f54d073aabe89c02a9dc6fe8331900e47946b18a","datavalue":{"value":"The paper consists of two big parts, the first is a crash course in complex analysis, the second reports on the formalization of some of the proofs in the mechanized reasoning system HOL-light. In the first part, the authors introduce holomorphic functions and some of their surprising properties (when compared to their real counterparts), e.g., the identity principle. First the one-dimensional case and then some higher-dimensional theorems are introduced.  With these preliminaries the first and second theorem of Cartan are introduced -- that under certain weak conditions a holomorphic higher-dimensional map must be the identity map or it must be linear, respectively. Furthermore the proofs of these theorems are sketched. In addition, a theorem on an involution and a relationship of holomorphic automorphisms and M\u00f6bius transformations is given.  In the second part of the paper the HOL-light system and its extensive library on real and complex numbers are introduced. In order to prove Cartan's theorems, important properties such as the rule on the derivative of composed functions are introduced. The paper concludes with remarks on the de Bruijn factor (how much longer the formal proofs are compared to paper proofs), and the procedural (what is done to produce a proofs) versus declarative (how does the proof look like) style of proofs in formal systems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q438546$126E40BD-1BBE-4936-8BD4-88B2B87F4FBC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"80e987276e122a41f9b91b8b2fac713fac5a8dbb","datavalue":{"value":{"entity-type":"item","numeric-id":504392,"id":"Q504392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$8633F5D0-FD48-4612-AB4C-801C8E0E79F5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$2A618328-4FA8-4011-BD43-A5BFCE7650CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6551dec4b4fdfd7664d2cb53e531802f2761e471","datavalue":{"value":"32A99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$EC9FA55B-F18B-4A34-89F6-6963A029B764","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5d2479f82dc9dd2ec6fedce7fe952448442e28da","datavalue":{"value":"30C80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$F04BFBCE-77C4-4246-A7F6-ABF7562D5851","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be32470b1e2f32b93d3702547d278b7a0447f812","datavalue":{"value":"6062052","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$B9E43BBD-1CCF-48B4-89D2-C36EE38C135D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"326c300cf62efa849a7bdb94dd90663d744d9f5d","datavalue":{"value":"formal proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q438546$882CD4C6-ED89-49C7-A295-720AD5C13128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b54d9de6499a9187e25e8189dec316bec96b816f","datavalue":{"value":"complex analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q438546$54D4F7EC-55DC-4E27-8062-887DDB5E0F9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dba02327bcf79dc25ac3ce521759b6969fc519f7","datavalue":{"value":"Cartan fixed point theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q438546$ACA0F65D-F523-406E-9255-519D4B1D1630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f0c853343c5586b4b10fb2b50abce16ecdc2adf","datavalue":{"value":"HOL-light","type":"string"},"datatype":"string"},"type":"statement","id":"Q438546$0A0DE240-E24D-4598-A034-4E6931072A5A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$DCD9E018-38FD-4811-908F-3FC02CD922FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$25E11727-CAF8-42C2-8CA5-0D51332868F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$94EB24E4-7040-4CFF-93C5-18D8A21C9B5D","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":"Q438546$8BDCD501-1486-4BA5-B790-D60637493D84","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"18fed01f6f3849700d9dbb8b2f61bbb2d54f8f41","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9198-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q438546$95515C8B-03CE-4445-9D21-3F72F2427451","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"08c1569bf426c944411461f84572aebb555d5023","datavalue":{"value":"W2135745323","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$EE4EEF24-C09A-44A2-B5BC-4AC199047F60","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6a561b9af459f6c8c57b4a4449f46fb1ee148f","datavalue":{"value":{"entity-type":"item","numeric-id":4305907,"id":"Q4305907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$C63851F1-8547-481A-85B1-85BED0814367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b040643183ce8f891afbe1850e8fa5bf9920e35","datavalue":{"value":{"entity-type":"item","numeric-id":1565609,"id":"Q1565609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$CC910E1E-630E-4C16-B773-305551B07DA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35657fcc9ea1aa63e2395ccdae7064ce285da058","datavalue":{"value":{"entity-type":"item","numeric-id":734831,"id":"Q734831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$F26FDA75-FDA0-4915-9521-5FD9398C189B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b06809062082b8f9f5dbc080e3987837376fa3d","datavalue":{"value":{"entity-type":"item","numeric-id":3499750,"id":"Q3499750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$ECA6BEEB-8242-441B-91E5-FE39CFB3FAFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"038d71599297a0253614efeeaeb4da386244dac4","datavalue":{"value":{"entity-type":"item","numeric-id":3892778,"id":"Q3892778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$D15FF9AA-1409-429A-BDDA-95BBA6061CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39f9c790d840262781bd5c02b6fba74083658746","datavalue":{"value":{"entity-type":"item","numeric-id":1840438,"id":"Q1840438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$FA24D618-08E1-4D1C-9C0E-1D56FDE6EE30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4cf44dc6c379b1f1a9b2c5baec2d960d5f32396","datavalue":{"value":{"entity-type":"item","numeric-id":661301,"id":"Q661301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$4170A701-731D-4ADB-A1F9-4130A17A3597","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b81ed5726d481fdb85841c4dfa3b274389260f","datavalue":{"value":{"entity-type":"item","numeric-id":5192393,"id":"Q5192393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$9D5A3906-8A07-429C-9DAF-10AE9977B087","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88f838c9d31bade5107439f0c0fe27ce86af2b82","datavalue":{"value":{"entity-type":"item","numeric-id":2495713,"id":"Q2495713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$E2E30125-3781-4AD2-A80D-59809995AF26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f67588ad9006460ff235350639496623b6f102fa","datavalue":{"value":{"entity-type":"item","numeric-id":2456222,"id":"Q2456222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$4B61C03E-2743-43CC-BD40-B8ED7021CEA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d9190693f3924b86be7203c014f0b8b161bc6f8","datavalue":{"value":{"entity-type":"item","numeric-id":5302559,"id":"Q5302559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$5AE0A35B-45E0-4C68-B63A-5EB0831EB812","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55a5c491e27bbeea4d7b95894d477a28fdcc0015","datavalue":{"value":{"entity-type":"item","numeric-id":5302558,"id":"Q5302558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$77CC4914-F9B8-432F-9A4B-338DA62764CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$020AF7B6-4857-4C3E-9AB4-876268225A66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"906baf24b37bdd520cca8517bf95cb9a9d93ebb6","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$325EB396-B545-4F0F-8838-FFE2F595FC7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25019528ec1858086747475c5735bfd3fb20bd44","datavalue":{"value":{"entity-type":"item","numeric-id":2527319,"id":"Q2527319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$3F91FB46-818D-42D5-94BE-A8DEECC156C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25c8a6f2a3af7004b88c557f1e1ff3593cf2e5ce","datavalue":{"value":{"entity-type":"item","numeric-id":3958740,"id":"Q3958740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$2C8600CA-33B0-4547-B5C8-D686B07FD0B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d25fa3320df2a62bc1669e2fe76fa9fe3f625eec","datavalue":{"value":{"entity-type":"item","numeric-id":4183557,"id":"Q4183557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$C1A9571D-37E2-4C71-8C1A-3D0E8F597978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10362950f34e98f922c4896b41a99f6667cd7c48","datavalue":{"value":{"entity-type":"item","numeric-id":3995636,"id":"Q3995636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$37089B1D-AE19-4261-898B-5794CD2AF97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"502ad8224b7ee39a96e36cfcfba1b8b740baa8c6","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$C9F55ED1-70AB-4903-88F1-AA696845E898","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b5045e17431ae100adc29ee6860720ac72d87fa","datavalue":{"value":{"entity-type":"item","numeric-id":5302561,"id":"Q5302561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438546$DEA4C24C-DC31-4C64-9D80-84D708CB3299","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ce80e9170a521a60c6d86642ea463c950e70eb99","datavalue":{"value":"10.1007/S10817-010-9198-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438546$163F00CD-01EF-4A66-951B-C825036F03AE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5917cef10283768771f78eab4f40635731cd570e","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9f93736113a348962ef98d7519d8dffb51ba1c6","datavalue":{"value":{"amount":"+0.7272322773933411","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438546$385D6F85-3926-4F0B-BA3B-D837FB948DBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"030a8e9ac6fc09570217d40508a4a4eabc57af6f","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40af42f6f85190dc76194b1e0a12d234e2ba9848","datavalue":{"value":{"amount":"+0.705115795135498","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438546$83C66A36-135C-4816-A4C9-FB6449212ED4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"647c8d4704e4e1c63c4d44857f4efc2289373760","datavalue":{"value":{"entity-type":"item","numeric-id":682381,"id":"Q682381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1dbeeaa7a54dd186da9b8925ea4d5a1245818193","datavalue":{"value":{"amount":"+0.6960033774375916","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438546$00A21850-6336-4F15-B196-952D685CEAE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6122a463333ca6ac1588dfc5fdebd5f2726a0c2","datavalue":{"value":{"entity-type":"item","numeric-id":1099303,"id":"Q1099303"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8469f3ee29139850bc8f4c27ec1ba8a96a7e68fc","datavalue":{"value":{"amount":"+0.6959133744239807","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438546$7C8FB519-E05B-4B3A-AB4E-F494E8FFB6E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d02279bac1d796a4fe3c783aac3fb822a5d0f319","datavalue":{"value":{"entity-type":"item","numeric-id":5270144,"id":"Q5270144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"090470da3f6be32cde70736d16064d3fef17bb5c","datavalue":{"value":{"amount":"+0.6955645680427551","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q438546$C8075515-7CCC-4A45-BFF0-1383BF181E14","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A certified proof of the Cartan fixed point theorems","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_certified_proof_of_the_Cartan_fixed_point_theorems"}}}}}