[Merged by Bors] - feat : port Algebra.GroupPower.Basic#874
[Merged by Bors] - feat : port Algebra.GroupPower.Basic#874
Conversation
|
This fails on |
|
Removed some |
|
(couldn't commit the raw |
| · rw [Nat.mul_zero, pow_zero, pow_zero] | ||
| · rw [Nat.mul_succ, pow_add, pow_succ', ih] | ||
|
|
||
| @[to_additive mul_nsmul] |
There was a problem hiding this comment.
Should this be @[to_additive mul_smul'] and the attribute above should also be changed?
There was a problem hiding this comment.
I did this, and left a porting note.
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
…r-community/mathlib4 into port-algebra-group_power-basic
|
There are lots of additional #aligns needed for the @[to_additive] versions. Hopefully this will be automated in mathport later: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.23align.20and.20to_additive. But for now we just need to do it by hand. :-( |
Thanks! I didn't really get the memo that we have to add all aligns generally instead of just the ones that deviate from the synport-generated ones. |
|
Thanks for those, hadn't touched the comments and docstsrings yet. |
We don't really need to add all of them. It seems we've just decided it's much easier to review / help out others PRs / maintain later, if all #align's are there. |
|
bors merge |
mathlib3 SHA: 9b2660e1b25419042c8da10bf411aa3c67f14383 Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded:
|
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following PRs: * `algebra.euclidean_domain.defs`: leanprover-community/mathlib4#871 * `algebra.group.ext`: leanprover-community/mathlib4#850 * `algebra.group_power.basic`: leanprover-community/mathlib4#874 * `algebra.hom.equiv.units.basic`: leanprover-community/mathlib4#895 * `algebra.hom.equiv.units.group_with_zero`: leanprover-community/mathlib4#901 * `algebra.order.group.instances`: leanprover-community/mathlib4#890 * `algebra.order.group.order_iso`: leanprover-community/mathlib4#895 * `algebra.order.group.units`: leanprover-community/mathlib4#898 * `algebra.order.monoid.nat_cast`: leanprover-community/mathlib4#893 * `algebra.order.monoid.type_tags`: leanprover-community/mathlib4#873 * `algebra.order.monoid.units`: leanprover-community/mathlib4#873 * `algebra.order.zero_le_one`: leanprover-community/mathlib4#893 * `combinatorics.quiver.push`: leanprover-community/mathlib4#868 * `control.traversable.basic`: leanprover-community/mathlib4#788 * `data.sum.order`: leanprover-community/mathlib4#880 * `group_theory.group_action.option`: leanprover-community/mathlib4#884 * `group_theory.group_action.sigma`: leanprover-community/mathlib4#885 * `group_theory.group_action.sum`: leanprover-community/mathlib4#882 * `group_theory.group_action.units`: leanprover-community/mathlib4#878 * `order.antisymmetrization`: leanprover-community/mathlib4#876
* `one_zsmul` and `zsmul_zero` were added for real in #874, so we no longer need to stub them out. * We can now remove the sorries in `zero_smulg` and `term_smul`.
mathlib3 SHA: 9b2660e1b25419042c8da10bf411aa3c67f14383