mathlib

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

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`