Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-19 09:36 6fbcc04a

View on Github →

feat(tactic/reassoc_axiom): produce associativity-friendly lemmas in category theory (#1341)

Estimated changes

Modified docs/tactics.md

Modified src/category_theory/adjunction/basic.lean

modified theorem category_theory.adjunction.counit_naturality

deleted theorem category_theory.adjunction.counit_naturality_assoc

modified theorem category_theory.adjunction.left_triangle_components

deleted theorem category_theory.adjunction.left_triangle_components_assoc

modified theorem category_theory.adjunction.right_triangle_components

deleted theorem category_theory.adjunction.right_triangle_components_assoc

modified theorem category_theory.adjunction.unit_naturality

deleted theorem category_theory.adjunction.unit_naturality_assoc

Modified src/category_theory/eq_to_hom.lean

modified theorem category_theory.eq_to_hom_trans

deleted theorem category_theory.eq_to_hom_trans_assoc

Modified src/category_theory/isomorphism.lean

deleted theorem category_theory.iso.hom_inv_id_assoc

deleted theorem category_theory.iso.inv_hom_id_assoc

Modified src/category_theory/limits/limits.lean

modified theorem category_theory.limits.colim.ι_map

deleted theorem category_theory.limits.colim.ι_map_assoc

modified theorem category_theory.limits.colimit.ι_desc

deleted theorem category_theory.limits.colimit.ι_desc_assoc

modified theorem category_theory.limits.colimit.ι_post

deleted theorem category_theory.limits.colimit.ι_post_assoc

modified theorem category_theory.limits.colimit.ι_pre

deleted theorem category_theory.limits.colimit.ι_pre_assoc

Created src/tactic/reassoc_axiom.lean