TY  - RPRT
TI  - The Banach lattice Lean library
AU  - David Muñoz-Lahoz
PY  - 2026
UR  - https://arxiv.org/abs/2608.07388
ID  - 2608.07388
ER  -