Lean Formalization

Formalization of some mathematical results using Lean 4 and Mathlib. See the repository

HTML-rendered Lean proofs:

Formalization of some results of the book Éléments d'Analyse Fonctionnelle by Francis Hirsch and Gilles Lacombe.
Formalization of the representation of finite groups as Cayley's graphs.
Formalization of the measure representation of ultrafilters.
Formalization of the total law of expectation/probability.