Formalization of the Solution to the Hopf Problem

A formalization of the resolution of the Hopf problem: the six-sphere admits a complex manifold structure compatible with its standard topology - plby/HopfProblem