Commit 2024-11-19 17:43 7242600f

feat: quantales (#17289) First definition of Quantales - a non-commutative generalization of Locales/Frames. There are still some points of discussion, which would require changes elsewhere in Mathlib, but this definition should be workeable as a starting point (I think). It's my first PR, but I've tried to stay close to what I've seen in CompleteLattices.