New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: add #align statements for to_additive decls #1816
Conversation
jcommelin
commented
Jan 24, 2023
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is clearly good, and should be merged quickly once it compiles.
bors d+
@@ -91,11 +91,10 @@ theorem image2_smul : image2 SMul.smul s t = s • t := | |||
#align set.image2_smul Set.image2_smul | |||
#align set.image2_vadd Set.image2_vadd | |||
|
|||
@[to_additive add_image_prod] | |||
-- @[to_additive add_image_prod] -- Porting note: bug in mathlib3 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This inserts a translation to an existing but unrelated declaration? We should probably make this @[to_additive vadd_image_prod]
if that works
@@ -95,7 +95,7 @@ theorem le_map_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAddHom | |||
(a b : α) : f a ≤ f b + f (a / b) := by | |||
simpa only [add_comm, div_mul_cancel'] using map_mul_le_add f (a / b) b | |||
#align le_map_add_map_div le_map_add_map_div | |||
#align le_map_add_map_sub le_map_add_map_sub | |||
-- #align le_map_add_map_sub le_map_add_map_sub -- Porting note: TODO: `to_additive` clashes |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, these are two declarations with the same additive version? Yeah, that happens sometimes.
✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>