mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

refactor(data/int/cast): Use hom classes

Open YaelDillies opened this issue 3 years ago • 6 comments

Restate lemmas using monoid_with_zero_hom_class/ring_hom_class instead of monoid_with_zero_hom/ring_hom.

  • [ ] depends on: #15985

Open in Gitpod

YaelDillies avatar Aug 12 '22 11:08 YaelDillies

Cc @urkud who was going to do this

ericrbg avatar Aug 12 '22 13:08 ericrbg

Please don't do map_inv/map_div/map_units_inv in the same PR. I've started #15985 about these lemmas, and already fixed more files (also, my map_units_inv is more general).

urkud avatar Aug 12 '22 21:08 urkud

It will be painful to undo, so I will just wait for yours to go through.

YaelDillies avatar Aug 12 '22 21:08 YaelDillies

I'll try to fix my branch while waiting for the next flight (I have about 4h).

urkud avatar Aug 12 '22 23:08 urkud

Safe flight!

ericrbg avatar Aug 12 '22 23:08 ericrbg

My PR is ready.

urkud avatar Aug 15 '22 11:08 urkud

This PR/issue depends on:

  • ~~leanprover-community/mathlib#15985~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Aug 16 '22 04:08 mathlib-dependent-issues-bot

@YaelDillies Could you please list API changes in the commit message?

urkud avatar Aug 20 '22 23:08 urkud

Otherwise LGTM. Thanks! bors d+

urkud avatar Aug 21 '22 01:08 urkud

:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Aug 21 '22 01:08 bors[bot]

That became minimal after your PR, thanks!

bors merge

YaelDillies avatar Aug 21 '22 06:08 YaelDillies

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Aug 21 '22 09:08 bors[bot]