Formalising the Krull Topology in Lean. - Sébastian Monnet (CoRR, 2022)