mathlib3
e2da6ab4 - port necessary things from lean-liquid to instantiate ab5 AddCommGroup

Commit
3 years ago
port necessary things from lean-liquid to instantiate ab5 AddCommGroup
References
Author
Parents
Loading