mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/ring/aut): add apply_mul_semiring_action & mul_semiring_action.to_ring_aut

Open mkaratarakis opened this issue 3 years ago • 4 comments

Open in Gitpod

mkaratarakis avatar Oct 07 '22 19:10 mkaratarakis

The linter is unhappy.

jcommelin avatar Oct 11 '22 06:10 jcommelin

OK, thank you. I think I fixed the linter issue. Is there something else I should do?

mkaratarakis avatar Oct 11 '22 11:10 mkaratarakis

@eric-wieser , the linter is now complaining about the universes. I am not sure what's the best approach here

mkaratarakis avatar Oct 11 '22 16:10 mkaratarakis

OK, thank you. I 've pushed these changes- let me know if there is anything else I should do. Furthermore, please take a look at #16850. I pushed the code and it keeps failing.

mkaratarakis avatar Oct 13 '22 17:10 mkaratarakis

Done, thank you. I've added all your suggestions.

mkaratarakis avatar Oct 14 '22 14:10 mkaratarakis

Thanks!

bors d+

Feel free to merge once CI is happy

eric-wieser avatar Oct 14 '22 14:10 eric-wieser

:v: mkaratarakis 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 Oct 14 '22 14:10 bors[bot]

Great, thank you

mkaratarakis avatar Oct 14 '22 16:10 mkaratarakis

bors merge

eric-wieser avatar Oct 15 '22 04:10 eric-wieser

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Oct 15 '22 10:10 bors[bot]