{"entities":{"Q7361850":{"pageid":31521089,"ns":120,"title":"Item:Q7361850","lastrevid":105369485,"modified":"2026-10-07T13:38:00Z","type":"item","id":"Q7361850","labels":{"en":{"language":"en","value":"The Hermite\u2013Lindemann\u2013Weierstra\u00df Transcendence Theorem"}},"descriptions":{"en":{"language":"en","value":"AFP entry Hermite_Lindemann"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"70b48027583f4113332f45ff20ea90824a45c393","datavalue":{"value":"https://isa-afp.org/entries/Hermite_Lindemann.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361850$D52C5AA5-B96E-4EFB-A1AA-795C71F0E152","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e013eff0176c277e28c34bb2d5686f71705cd92d","datavalue":{"value":{"time":"+2021-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361850$C35D1DF7-E175-45DA-AB16-57974EF7E670","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"85859c7ab42dcb8b36208f2902b7ce0d86423a6f","datavalue":{"value":"Manuel Eberl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361850$112FFB8F-4AFA-447E-8756-8DF463040CB7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"885da06ab2502925dc5ea3a082d3b1d9304a4f0b","datavalue":{"value":{"text":"The Hermite\u2013Lindemann\u2013Weierstra\u00df Transcendence Theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361850$2C90AFBD-585B-4240-AB53-0EAECB8006DC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5df94dba06e1eb2fd4143f6a8dc02813602341f0","datavalue":{"value":"This article provides a formalisation of the Hermite-Lindemann-Weierstra\u00df Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstra\u00df). This theorem is one of the crowning achievements of 19th century number theory. The theorem states that if $\\alpha_1, \\ldots, \\alpha_n\\in\\mathbb{C}$ are algebraic numbers that are linearly independent over $\\mathbb{Z}$, then $e^{\\alpha_1},\\ldots,e^{\\alpha_n}$ are algebraically independent over $\\mathbb{Q}$. Like the previous formalisation in Coq by Bernard , I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers $\\beta_1, \\ldots, \\beta_n\\in\\mathbb{C}$ and distinct algebraic numbers $\\alpha_i, \\ldots, \\alpha_n\\in\\mathbb{C}$, we have $\\beta_1 e^{\\alpha_1} + \\ldots + \\beta_n e^{\\alpha_n} = 0$ if and only if all the $\\beta_i$ are zero. This has a number of direct corollaries, e.g.: $e$ and $\\pi$ are transcendental $e^z$, $\\sin z$, $\\tan z$, etc. are transcendental for algebraic $z\\in\\mathbb{C}\\setminus\\{0\\}$ $\\ln z$ is transcendental for algebraic $z\\in\\mathbb{C}\\setminus\\{0, 1\\}$","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361850$0B8BE1D9-BBD4-4B71-9E0B-E69AD4950724","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c15c65f7cb4bb603b7e190ecae8ab47753e2f970","datavalue":{"value":{"entity-type":"item","numeric-id":4050665,"id":"Q4050665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$AB1D5740-81FF-44DD-8CAD-F7502A6BB4A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"251deab27946b94aed7cdb38a767b41b4f2b8107","datavalue":{"value":{"entity-type":"item","numeric-id":1687717,"id":"Q1687717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$71F52052-7E5A-45F3-839F-CDBA98F1BBC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"076ceef7206a7113473e93e7ea3ed537158d4981","datavalue":{"value":{"entity-type":"item","numeric-id":2649766,"id":"Q2649766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$2863A1AA-4669-415B-AAEC-27AE335CF750","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":"Q7361850$BE18596E-FD8D-4F7D-A7AA-7C6580F95E9F","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"2594c168cd7f73433095d3ad9eaea472f82c3ee0","datavalue":{"value":{"entity-type":"item","numeric-id":7361619,"id":"Q7361619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$7DA3C61F-EB8C-47B2-A9A8-5B2EF8A5FFA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"f2cc167c5c3e4741916dd4301ce656ac6bd5f361","datavalue":{"value":{"entity-type":"item","numeric-id":7361352,"id":"Q7361352"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$5A5CFD14-EBE3-4621-832D-C872021CA852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"d20e33c5201365c1e89ae8eda05b1704f33818bc","datavalue":{"value":{"entity-type":"item","numeric-id":7361716,"id":"Q7361716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$F604EFEA-EB44-4BEF-9323-187B0225358F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"51467ee0a503af56d0e1903e0514853bd73fc1a9","datavalue":{"value":{"entity-type":"item","numeric-id":7360830,"id":"Q7360830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361850$D7E7F2AB-569C-42B5-A1F8-8FF613C9BDE9","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":"Q7361850$97A6BEF1-8DFC-4DFA-A56C-298C59F56CCF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The Hermite\u2013Lindemann\u2013Weierstra\u00df Transcendence Theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_Hermite%E2%80%93Lindemann%E2%80%93Weierstra%C3%9F_Transcendence_Theorem"}}}}}