Commit 2024-05-22 07:28 49465dde

View on Github →

chore(Algebra/Category): make coe_of a simp lemma in CommGroupCat (#13055) This tried to make the concrete category developments more uniform: whether coe_of was a simp lemma or not seems to have been decided differently in different files during porting. Also adds some lemmas to improve confluence.

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Adjunctions.lean

Modified Mathlib/Algebra/Category/GroupCat/Basic.lean

modified theorem AddCommGroupCat.asHom_apply

added theorem CommGroupCat.coe_comp'

added theorem CommGroupCat.coe_id'

added theorem GroupCat.coe_comp'

added theorem GroupCat.coe_id'

Modified Mathlib/Algebra/Category/GroupCat/Biproducts.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

Modified Mathlib/Algebra/Homology/ShortComplex/Ab.lean

Modified Mathlib/CategoryTheory/Galois/Prorepresentability.lean