commutative residual algebras

Stream: mathlib4

[Jakob von Raumer]

Has anyone looked at formalizing van Oostrom et al.'s "commutative residual algebras" as way to capture e.g.

• Difference of sets
• Nat.sub

Could remove some "code duplication" from mathlib, though I'm not sure if the benefit is big enough...

[Yaël Dillies]

At first sight, it looks like a generalisation which won't be helpful in practice as it unifies notations and lemmas that

1. are very widespread
2. are very different in their use by mathematicians

[Yaël Dillies]

Would be fun to formalise them in their own right, though

[Jakob von Raumer]

Yea, I guess generalizing all the lemmas to type class would also cause names to be quite confusing...