Theorem Path.Homotopic.map_trans_evalAt

Modification history

2026-01-08 12:28
Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
feat(FundamentalGroupoid/InducedMaps): generalize to different universes (#33445) …
Added Path.Homotopic.map_trans_evalAtView on Github →