Skip to content

Commit 561cc19

Browse files
themathqueenb-mehta
authored andcommitted
chore(RingTheory/Bialgebra/Hom): toCoalgHom as prefix for simps (leanprover-community#39552)
There are currently no generated `simps` lemmas for these, so this is a straightforward change.
1 parent 629354a commit 561cc19

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/RingTheory/Bialgebra/Hom.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ def Simps.apply {R α β : Type*} [CommSemiring R]
133133
[Algebra R β] [CoalgebraStruct R α] [CoalgebraStruct R β]
134134
(f : α →ₐc[R] β) : α → β := f
135135

136-
initialize_simps_projections BialgHom (toFun → apply)
136+
initialize_simps_projections BialgHom (toFun → apply, as_prefix toCoalgHom)
137137

138138
@[simp]
139139
protected theorem coe_coe {F : Type*} [FunLike F A B] [BialgHomClass F R A B] (f : F) :

0 commit comments

Comments
 (0)