mathlib
65bf1349
- split(algebra/hom/ring): Split off `algebra.ring.basic` (#14144)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
split(algebra/hom/ring): Split off `algebra.ring.basic` (#14144) Move `non_unital_ring_hom` and `ring_hom` to a new file `algebra.hom.ring`. Crediting * Amelia for #1305 * Jireh for #13430
Author
YaelDillies
Parents
4ae5e7a0
Loading