Formalizing Homology

Sebastian Koch fly.high.android _AT_ gmail.com <[email protected]> Sun, 3 Nov 2024 05:47:46 +0100

Newsgroups	gmane.comp.mathematics.mizar
Message-ID	<[email protected]>

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