Hi there,I'm trying out formalizing Homology groups following Allen Hatcher's Algebraic Topology.
I wanted to know if there are others making an effort in this direction, maybe we can work together?
Also there is a chance I completely missed the formalization in the MML. Where are the unit vectors for RealLinearSpace anyway?
Best regards and stay healthy Sebastian Koch