mathlib

2dc24f48 - quotient by the kernel of the laplacian