mathlib3
b54960d1 - refactor(*): migrate some files to bundled ring homs (#2133)

Commit
5 years ago
refactor(*): migrate some files to bundled ring homs (#2133) * refactor(*): migrate some files to bundled ring homs * Rename ring_hom.is_local back to is_local_ring_hom * Apply suggestions from code review Co-Authored-By: Johan Commelin <johan@commelin.net> * Restore 2 instances, make `map` use bundled homs * More bundled homs * Add a docstring Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading