Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-05 17:04 6ed79339

View on Github →

feat(combinatorics/quiver/*) cast arrows and paths along equalities (#17617) Authored-by: Antoine Labelle antoinelab01@gmail.com

Estimated changes

Modified src/combinatorics/quiver/basic.lean

added theorem prefunctor.comp_id

added theorem prefunctor.id_comp

Created src/combinatorics/quiver/cast.lean

added theorem quiver.cast_eq_of_cons_eq_cons

added theorem quiver.eq_nil_of_length_zero

added def quiver.hom.cast

added theorem quiver.hom.cast_cast

added theorem quiver.hom.cast_eq_cast

added theorem quiver.hom.cast_eq_iff_heq

added theorem quiver.hom.cast_heq

added theorem quiver.hom.cast_rfl_rfl

added theorem quiver.hom.eq_cast_iff_heq

added theorem quiver.hom_cast_eq_of_cons_eq_cons

added def quiver.path.cast

added theorem quiver.path.cast_cast

added theorem quiver.path.cast_cons

added theorem quiver.path.cast_eq_cast

added theorem quiver.path.cast_eq_iff_heq

added theorem quiver.path.cast_heq

added theorem quiver.path.cast_nil

added theorem quiver.path.cast_rfl_rfl

added theorem quiver.path.eq_cast_iff_heq

Modified src/combinatorics/quiver/path.lean

added theorem quiver.path.cons_ne_nil

added theorem quiver.path.heq_of_cons_eq_cons

added theorem quiver.path.hom_heq_of_cons_eq_cons

added theorem quiver.path.nil_ne_cons

added theorem quiver.path.obj_eq_of_cons_eq_cons