Commit 2023-03-23 16:06 d1cfe4d7

View on Github →

feat: port CategoryTheory.Groupoid.VertexGroup (#2609)

depends on: #2883

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Groupoid/VertexGroup.lean

added def CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup

added theorem CategoryTheory.Groupoid.vertexGroup.inv_eq_inv

added def CategoryTheory.Groupoid.vertexGroupIsomOfMap

added def CategoryTheory.Groupoid.vertexGroupIsomOfPath