mathlib
ae17d05f
- chore(algebra/hom/non_unital_alg): add missing `non_unital_ring_hom_class` instance (#16783)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(algebra/hom/non_unital_alg): add missing `non_unital_ring_hom_class` instance (#16783) This instance was missing because `non_unital_alg_hom` was defined before `non_unital_ring_hom`.
Author
j-loreaux
Parents
8f83c26d
Loading