Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 11:12 6a51706d

View on Github →

chore(topology/homotopy): Move more algebraic-flavored content about fundamental groupoid to algebraic_topology folder (#12631) Moved:

  • topology/homotopy/fundamental_groupoid.lean to algebraic_topology/fundamental_groupoid/basic.lean
  • the second half of topology/homotopy/product.lean, dealing with fundamental_groupoid_functor preserving products, to algebraic_topology/fundamental_groupoid/product.lean
  • topology/homotopy/induced_maps.lean to algebraic_topology/fundamental_groupoid/induced_maps.lean

Estimated changes