are quotient groups in mathlib

Stream: maths

[Johan Commelin]

I now have a complex. I want to take its homology. I can't find quotient groups in mathlib. What is the best way forward? Should I define them myselves, or should I cast to modules?

[Kenny Lau]

you should define them yourself