Theorem Path.Homotopic.Quotient.refl_trans

Modification history

2025-11-18 12:49
Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
feat: lemmas for paths-up-to-homotopy (#31574) …
Added Path.Homotopic.Quotient.refl_transView on Github →