mathlib
f7fe7dd0 - refactor(ring_theory/free_comm_ring): don't use is_ring_hom (#13352)

Commit

3 years ago

refactor(ring_theory/free_comm_ring): don't use is_ring_hom (#13352) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents