{"entities":{"Q7361145":{"pageid":31518974,"ns":120,"title":"Item:Q7361145","lastrevid":105363251,"modified":"2026-10-07T13:34:47Z","type":"item","id":"Q7361145","labels":{"en":{"language":"en","value":"Lucas's Theorem"}},"descriptions":{"en":{"language":"en","value":"AFP entry Lucas_Theorem"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"58b757380dd8ca2451af1866d265220e62a31d63","datavalue":{"value":"https://isa-afp.org/entries/Lucas_Theorem.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361145$27A47669-3005-4645-BAF1-AD77496195F3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5583640b16c3225e3c55a84532f843da9ad4b6cf","datavalue":{"value":{"time":"+2020-04-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361145$5715933A-AE1B-4D78-B6E3-58164016BF47","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"1f5398cfc166ea4dddf107332321d7745473ad76","datavalue":{"value":"Chelsea Edmonds","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361145$F83D4262-972A-4E6A-BA35-F3A58D64A92C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"be34ca634b219b77cae6e5707fb845c49ff5444c","datavalue":{"value":{"text":"Lucas's Theorem","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361145$CD98547E-D28D-499E-9A26-16884397217C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"3c93024cf52fe741ef8d7d497dff8656081dc901","datavalue":{"value":"This work presents a formalisation of a generating function proof for Lucas's theorem. We first outline extensions to the existing Formal Power Series (FPS) library, including an equivalence relation for coefficients modulo n , an alternate binomial theorem statement, and a formalised proof of the Freshman's dream (mod p ) lemma. The second part of the work presents the formal proof of Lucas's Theorem. Working backwards, the formalisation first proves a well known corollary of the theorem which is easier to formalise, and then applies induction to prove the original theorem statement. The proof of the corollary aims to provide a good example of a formalised generating function equivalence proof using the FPS library. The final theorem statement is intended to be integrated into the formalised proof of Hilbert's 10th Problem.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361145$602784FE-A03B-4864-AEB6-85C97747D8DC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa37805d7534f453770c465fa7c972c5494b9110","datavalue":{"value":{"entity-type":"item","numeric-id":5875447,"id":"Q5875447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361145$D799486F-4C4F-4086-8083-AF537A92A0D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a55447afe9e55109d21f7cb3e3fc40d677697651","datavalue":{"value":{"entity-type":"item","numeric-id":5891671,"id":"Q5891671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361145$9EAE756F-5BC5-4174-ADF4-3699DD47F8B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1133187e1625c43367ceb6961acd1a5a3b5e33bc","datavalue":{"value":{"entity-type":"item","numeric-id":5786066,"id":"Q5786066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361145$D541EDE4-703F-4239-9B13-1AB01BC0C58E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9f3d1ae30c91383ada80e5423ca9f4c05b9f2dc","datavalue":{"value":{"entity-type":"item","numeric-id":5277759,"id":"Q5277759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361145$FC141BEE-0DC9-49C2-A102-E755DC9109DC","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":"Q7361145$AB57831F-27D8-4984-BD87-8B4ABF7DF3EE","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":"Q7361145$77B3ED64-555E-4B37-8789-A31706388D92","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":"Q7361145$567F0EF1-F733-403D-B6BB-9B3186040D87","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Lucas's Theorem","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Lucas%27s_Theorem"}}}}}