Vector Lattices in Lean

Stream: new members

[David Muñoz Lahoz]

Hello everyone. I am David, a PhD student at Instituto de Ciencias Matemáticas (Madrid, Spain) working on Functional Analysis—Banach spaces, Banach lattices and related topics. To teach myself Lean, I formalized the Kakutani–Bohnenblust–Krein representation theorem, one of the main representation results in the theory of Banach lattices (Github repo).

I was wondering whether some of this material could be relevant for mathlib. For instance, I can see here that at least some of the properties that are proved for the absolute value in linearly ordered groups would actually hold in the more general (and natural) setting of lattice ordered groups. Would a contribution in this line be welcome?