Commit 2023-12-11 14:48 33095fed
View on Github →feat(RingTheory/Coalgebra): generalize the Finsupp instance (#8868)
The original Coalgebra R (ι →₀ R) is now recovered from [Coalgebra R A] : Coalgebra R (ι →₀ A) as a special case.
Salvaged from https://github.com/leanprover-community/mathlib4/pull/8621#discussion_r1408532458