BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Jonas van der Schaaf (Universität Münster)
DTSTART:20260119T151500Z
DTEND:20260119T154500Z
DTSTAMP:20260420T024856Z
UID:LT2026/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/3/">I
 nternal Projectivity of the Sequence Space in Lean</a>\nby Jonas van der S
 chaaf (Universität Münster) as part of Lean Together 2026\n\n\nAbstract\
 nThe theory of condensed mathematics has been well-explored in formalized 
 mathematics. In my master thesis\, I proved that the sequence space\, a co
 ndensed Abelian group describing null-sequences\, is internally projective
  in the category of light condensed abelian groups. I will discuss the pro
 of\, and what it is like for a relative beginner to prove a non-trivial th
 eorem in Lean.\n
LOCATION:https://researchseminars.org/talk/LT2026/3/
END:VEVENT
END:VCALENDAR