{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:02:03Z","timestamp":1748491323724,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_4","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"61-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Chaining Extensionality Lemmas in\u00a0Lean\u2019s Mathlib"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0412-4978","authenticated-orcid":false,"given":"Eric","family":"Wieser","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"The mathlib Community. \u201cThe Lean Mathematical Library\u201d. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. POPL \u201920: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages. New Orleans LA USA: ACM, Jan. 20, 2020, pp. 367\u2013381. isbn: 978-1-4503-7097\u20134. https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"4_CR3","unstructured":"Wieser, E.: Scalar actions in Lean\u2019s mathlib. In: Workshop Papers of the 14th Conference on Intelligent Computer Mathematics. CICM 2021, vol. 3377. Timisoara, Romania: CEUR-WS (2021). arXiv:2108. 10700 [cs.LO]"},{"key":"4_CR4","unstructured":"Sk\u0159ivan, T.: Lecopivo\/SciLean: Scientific Computing in Lean 4. https:\/\/github.com\/lecopivo\/SciLean. Accessed 18 Feb 02"},{"key":"4_CR5","unstructured":"Morrison, S.: chore: upstream \n\n                    \n                   tactic (2024). https:\/\/github.com\/leanprover\/lean4\/pull\/3306"},{"key":"4_CR6","unstructured":"Hudon, S.: feat(tactic\/ext): new \n\n                    \n                   tactic and corresponding \n\n                    \n                   Reviewed by Johannes H\u00f6lzl and Mario Carneiro (2018 ). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/104"},{"key":"4_CR7","unstructured":"Price, G.: chore(algebra\/direct_sum_graded): golf proofs. Reviewed by Eric Wieser and Scott Morrison (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/7029"},{"key":"4_CR8","unstructured":"Hughes, C.: feat(group_theory\/semidirect_product): \n\n                    \n                   and \n\n                    \n                  . Reviewed by Scott Morrison (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/3408"},{"key":"4_CR9","unstructured":"Topaz, A.: feat(linear_algebra\/tensor_algebra): Tensor algebras. Reviewed by Eric Wieser, Scott Morrison, Patrick Massot, Johan Commelin, and Chris Hughes (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/3531"},{"key":"4_CR10","unstructured":"Morrison, S.: feat(algebra\/ring_quot): quotients of noncommutative rings. Reviewed by Eric Wieser, Kenny Lau, and Johan Commelin (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/4078"},{"key":"4_CR11","unstructured":"Kudryashov, Y.G. chore(*): a few more type-specific ext lemmas. Reviewed by Johan Commelin and Eric Wieser (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/4741"},{"key":"4_CR12","unstructured":"Wieser, E.: feat(group_theory\/*): mark some lemmas as ext (about homs out of free constructions). Reviewed by Floris van Doorn (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/5484"},{"key":"4_CR13","unstructured":"Wieser, E.: feat(linear_algebra\/exterior_algebra): Add an exterior algebra. Reviewed by Anne Baanen and Scott Morrison (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/4297"},{"key":"4_CR14","unstructured":"Wieser, E.: feat(linear_algebra\/clifford_algebra): Add a definition derived from \n\n                    \n                  . Reviewed by Anne Baanen, Adam Topaz, Heather Macbeth, and Utensil Song (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/4430"},{"key":"4_CR15","unstructured":"Wieser, E.: feat(algebra\/direct_sum): graded algebras. Reviewed by Kevin Buzzard and Johan Commelin (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/8783"},{"key":"4_CR16","unstructured":"Wieser, E.: feat(data\/complex\/module): add \n\n                    \n                  . Reviewed by Anne Baanen (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/8105"},{"key":"4_CR17","unstructured":"Wieser, E.: feat(linear_algebra\/clifford_algebra\/equivs): There is a clifford algebra isomorphic to the dual numbers. Reviewed by Johan Commelin and Rob Lewis (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/10730"},{"key":"4_CR18","unstructured":"Wieser, E.: feat(algebra\/triv_sq_zero_ext): universal property. Reviewed by Johan Commelin (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/10754"},{"key":"4_CR19","unstructured":"Wieser, E.: feat(RingTheory\/TensorProduct): heterogenize. Reviewed by Johan Commelin and Antoine Chambert-Loir (2023). https:\/\/github.com\/leanprover-community\/mathlib4\/pull\/6417"},{"key":"4_CR20","unstructured":"Wieser, E.: feat(Data\/Polynomial\/AlgebraMap): more results for non-commutative polynomials. Reviewed by Ya\u00ebl Dillies and Johan Commelin (2023). https:\/\/github.com\/leanprover-community\/mathlib4\/pull\/8116"},{"key":"4_CR21","unstructured":"Wieser, E.: feat(data\/dfinsupp): Port over the \n\n                    \n                   API. Reviewed by Johan Commelin (2020). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/4821"},{"key":"4_CR22","unstructured":"Wieser, E.: refactor(linear_algebra\/tensor_product): Use a more powerful lemma for ext. Reviewed by Johan Commelin (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/6105"},{"key":"4_CR23","unstructured":"Wieser, E.: feat(linear_algebra\/prod): add an ext lemma that recurses into products. Reviewed by Johan Commelin (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/6124"},{"key":"4_CR24","unstructured":"Wieser, E.: feat(linear_algebra\/clifford_algebra\/of_alternating): extend alternating maps to the exterior algebra. Reviewed by Oliver Nash (2022). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/14803"},{"key":"4_CR25","unstructured":"Wieser, E.: feat(data\/zsqrtd\/to_real): Add \n\n                    \n                  . Reviewed by Johan Commelin, Mario Carneiro, Bryan Gin-ge Chen, and Anne Baanen (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/5640"},{"key":"4_CR26","unstructured":"Wieser, E.: feat(linear_algebra\/basic, group_theory\/quotient___group, algebra\/lie\/quotient): ext lemmas for morphisms out of quotients. Reviewed by Oliver Nash and Anne Baanen (2021). https:\/\/github.com\/leanprover-community\/mathlib\/pull\/8641"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:43Z","timestamp":1748412343000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}