Commit 2022-03-14 09:29 a2544deb
View on Github →chore(algebra/category/Module): simp lemmas for monoidal closed (#12608)
I'm worried by the fact that I can't express the coercions here without using @. They do turn up in the wild, however!
chore(algebra/category/Module): simp lemmas for monoidal closed (#12608)
I'm worried by the fact that I can't express the coercions here without using @. They do turn up in the wild, however!