Documentation

LeanPool.HopfProblem.HomologyOfX.TrianglePeriodFamilyHomologyAlgebra

Hopf problem: homology of x · triangle period family homology algebra #

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.TrianglePeriodFamilyHomologyAlgebra.range_eq_of_coordinates {H : Type u_1} [AddCommGroup H] [Module ℤ H] (f g : H × H →ₗ[ℤ] H) (e : (H × H) ≃ₗ[ℤ] H × H) (he : ∀ (x : H × H), f (e x) = g x) :