mathlib
51546d29 - chore(ring_theory/free_ring): use bundled ring homs (#4011)

Commit
5 years ago
chore(ring_theory/free_ring): use bundled ring homs (#4011) Use bundled ring homs in `free_ring` and `free_comm_ring`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading