BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:María Inés de Frutos Fernández (Imperial College London)
DTSTART:20220309T160000Z
DTEND:20220309T170000Z
DTSTAMP:20260418T063938Z
UID:LNTS/64
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LNTS/64/">Fo
 rmalizing the ring of adèles and some applications in Lean</a>\nby María
  Inés de Frutos Fernández (Imperial College London) as part of London nu
 mber theory seminar\n\n\nAbstract\nI will present a formalization of the r
 ing of adèles and group of idèles of a global field in the Lean 3 theore
 m prover. Lean is an interactive theorem prover with an ever-growing mathe
 matics library. I will give a quick introduction to Lean and explain how t
 hese definitions were formalized\, with a focus on the kind of decisions o
 ne has to make during the formalization process.\n\nBesides the definition
  of the adèles\, we will discuss the formalization of applications includ
 ing the statement of the main theorem of global class field theory and a p
 roof that the ideal class group of a number field is isomorphic to an expl
 icit quotient of its idèle class group.\n
LOCATION:https://researchseminars.org/talk/LNTS/64/
END:VEVENT
END:VCALENDAR