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] - feat(algebra/group_with_zero): add lemmas about f * pi.single i x
#6418
Conversation
@eric-wieser Should I close this PR? |
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.
Moved the lemmas, generalised them to dependent types and renamed them. I think it's good to go.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
LGTM! bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Sorry! bors d=@YaelDillies |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
…6418) Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
f * pi.single i x
f * pi.single i x
Match leanprover-community/mathlib#6418 * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`246f6f7989ff86bd07e1b014846f11304f33cf9e`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..246f6f7989ff86bd07e1b014846f11304f33cf9e)
Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841 * [`order.basic`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`order.monotone.basic`@`ac5a7cec422c3909db52e13dde2e729657d19b0e`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/monotone/basic?range=ac5a7cec422c3909db52e13dde2e729657d19b0e..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..90df25ded755a2cf9651ea850d1abe429b1e4eb1)
Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841 * [`order.basic`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`order.monotone.basic`@`ac5a7cec422c3909db52e13dde2e729657d19b0e`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/monotone/basic?range=ac5a7cec422c3909db52e13dde2e729657d19b0e..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..90df25ded755a2cf9651ea850d1abe429b1e4eb1)
Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841 * [`order.basic`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`order.monotone.basic`@`ac5a7cec422c3909db52e13dde2e729657d19b0e`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/monotone/basic?range=ac5a7cec422c3909db52e13dde2e729657d19b0e..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..90df25ded755a2cf9651ea850d1abe429b1e4eb1)
Match leanprover-community/mathlib#6418 and leanprover-community/mathlib#18841 * [`order.basic`@`210657c4ea4a4a7b234392f70a3a2a83346dfa90`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/basic?range=210657c4ea4a4a7b234392f70a3a2a83346dfa90..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`order.monotone.basic`@`ac5a7cec422c3909db52e13dde2e729657d19b0e`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/order/monotone/basic?range=ac5a7cec422c3909db52e13dde2e729657d19b0e..90df25ded755a2cf9651ea850d1abe429b1e4eb1) * [`algebra.group.pi`@`b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7`..`90df25ded755a2cf9651ea850d1abe429b1e4eb1`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/pi?range=b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7..90df25ded755a2cf9651ea850d1abe429b1e4eb1)
The code should be OK but @eric-wieser raised concerns about names and I agree that the names look odd. I won't need these functions in the nearest future, so I leave the decision to someone else.
Cherry-picked from #6390