Formalising Perfectoid Spaces

POPL 2020