[Merged by Bors] - chore: Nsmul -> NSMul, Zpow -> ZPow, etc#9067
[Merged by Bors] - chore: Nsmul -> NSMul, Zpow -> ZPow, etc#9067winstonyin wants to merge 11 commits intomasterfrom
Nsmul -> NSMul, Zpow -> ZPow, etc#9067Conversation
|
|
Mathlib/Algebra/Group/Defs.lean
Outdated
| /-- `a • b` computes the product of `a` and `b`. | ||
| The meaning of this notation is type-dependent, but it is intended to be used for left actions. -/ | ||
| hSMul : α → β → γ | ||
| hsmul : α → β → γ |
There was a problem hiding this comment.
| hsmul : α → β → γ | |
| hSMul : α → β → γ |
because this matches HMul.hMul, which is not something we have the power to change.
eric-wieser
left a comment
There was a problem hiding this comment.
Can you do a pass for Vadd -> VAdd too?
This reverts commit 210f14c.
|
@eric-wieser I do not find any instances of |
|
Currently there are some Set.vAddAssocClass that should be renamed to |
| @[to_additive vAddAssocClass] | ||
| @[to_additive vaddAssocClass] | ||
| instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : | ||
| IsScalarTower α β (Set γ) where | ||
| smul_assoc a b T := by simp only [← image_smul, image_image, smul_assoc] | ||
| #align set.is_scalar_tower Set.isScalarTower | ||
| #align set.vadd_assoc_class Set.vAddAssocClass | ||
| #align set.vadd_assoc_class Set.vaddAssocClass |
There was a problem hiding this comment.
Shouldn't we teach to_additive about this rule? What's the current auto-generated name? (You can find out using to_additive?.)
There was a problem hiding this comment.
Let's worry about that later.
maintainer merge
| ## Main definitions | ||
|
|
||
| - `ZMod.quotientZmultiplesNatEquivZMod` and `ZMod.quotientZmultiplesEquivZMod`: | ||
| - `ZMod.quotientZMultiplesNatEquivZMod` and `ZMod.quotientZMultiplesEquivZMod`: |
There was a problem hiding this comment.
So we're capitalizing AddSubgroup.zmultiples as ZMultiples. Looks good to me.
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
|
Pull request successfully merged into master. Build succeeded: |
Nsmul -> NSMul, Zpow -> ZPow, etcNsmul -> NSMul, Zpow -> ZPow, etc
Normalising to naming convention rule number 6.