Summable Family in a Commutative Group - Coghetto Roland (Formalized Mathematics, 2015)
Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [22], [7]. In this paper we present our formalization of this theory in Mizar [6].