Commit 2025-03-08 07:07 2186c5fb

View on Github →

feat: add some simp lemmas for FGModuleCat and FDRep (#22668) Add some simp lemmas to deal with FGModuleCat and FDRep.

Estimated changes

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

added theorem FGModuleCat.hom_comp

added theorem FGModuleCat.hom_id

added theorem FGModuleCat.obj_carrier

added theorem FGModuleCat.of_carrier

deleted theorem obj_carrier

Modified Mathlib/RepresentationTheory/FDRep.lean

added theorem FDRep.of_ρ'

added theorem FDRep.ρ_inv_self_apply

added theorem FDRep.ρ_self_inv_apply