mathlib

449e06a9 - feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182)

feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182) This pr adds the following helper functions for converting paths to and from elements of the fundamental group: - `to_arrow`: converts element of the fundamental group to an arrow in the fundamental groupoid - `to_path`: converts element of the fundamental group to a (quotient of homotopic) path in the space - `from_arrow`: constructs an element of the fundamental group from a self-arrow in the fundamental groupoid - `from_path`: constructs an element of the fundamental group from a (quotient of homotopic) path in the space These parallel the similarly named functions for the fundamental group [here](https://github.com/leanprover-community/mathlib/blob/743ed5d1dd54fffd65e3a7f3522e4a4e85472964/src/algebraic_topology/fundamental_groupoid/basic.lean#L339-L355). They will prove helpful in doing computations with the fundamental group later e.g. for the disk, circle, etc.