Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - refactor: use consistent names for forgetful smul structures #15500

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - refactor: use consistent names for forgetful smul structures #15500

wants to merge 6 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Aug 4, 2024 •
edited
Loading

Moves:

  • AddCommMonoid.natModule -> AddCommMonoid.toNatModule
  • AddCommGroup.intModule -> AddCommGroup.toIntModule
  • algebraNat -> Semiring.toNatAlgebra
  • algebraInt -> Ring.toIntAlgebra
  • algebraRat -> DivisionRing.toRatAlgebra
  • AddCommGroup.natModule.unique -> AddCommMonoid.uniqueNatModule
  • AddCommGroup.intModule.unique -> AddCommGroup.uniqueIntModule

The premise here is that the conversion from AddCommGroup to AddCommMonoid is not really any different from converting from AddCommGroup to Module ℤ; and so both should be named with the to* naming convention.

Tihs also brings the naming of the Module and Algebra instances into alignment.

I chose toNatModule instead of toModuleNat to match the prose, ℕ-module.
This fits a common naming convention if you view Module as infix, as we do with various other lean functions without actual infix notation.

Open in Gitpod

eric-wieser
eric-wieser commented Aug 4, 2024
View reviewed changes
Mathlib/Algebra/Algebra/Basic.lean
@@ -241,10 +241,10 @@ section Int
variable (R : Type*) [Ring R]

-- Lower the priority so that `Algebra.id` is picked most of the time when working with
-- `ℤ`-algebras. This is only an issue since `Algebra.id ℤ` and `algebraInt ℤ` are not yet defeq.
-- TODO: fix this by adding an `ofInt` field to rings.
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was fixed long ago :)

@github-actions GitHub Actions
Copy link

github-actions bot commented Aug 4, 2024 •
edited
Loading

PR summary 778dc7c525

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ AddCommGroup.toIntModule
+ AddCommGroup.toNatModule
+ AddCommGroup.uniqueIntModule
+ AddCommMonoid.uniqueNatModule
+ DivisionRing.toRatAlgebra
+ instance (priority := 99) Ring.toIntAlgebra : Algebra ℤ R
+ instance (priority := 99) Semiring.toNatAlgebra : Algebra ℕ R
++ DivisionRing.toRatAlgebra.
- AddCommGroup.intModule
- AddCommGroup.intModule.unique
- AddCommMonoid.natModule
- AddCommMonoid.natModule.unique
- algebraRat
- instance (priority := 99) algebraInt : Algebra ℤ R
- instance (priority := 99) algebraNat : Algebra ℕ R
-- algebraRat.

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@eric-wieser eric-wieser changed the title refactor: use consistent names for forgetful modules structures refactor: use consistent names for forgetful smul structures Aug 4, 2024
@YaelDillies
Copy link
Collaborator

Should toNatModule be toModuleNat, while we are at it?

@eric-wieser
Copy link
Member Author

eric-wieser commented Aug 4, 2024 •
edited
Loading

I'd argue no, because NatModule is much closed to the prose, " $\mathbb{N}$-module".

(And this fits the Lean naming convention if you view Module as infix like Nat.choose)

@eric-wieser eric-wieser added the t-algebra Algebra (groups, rings, fields, etc) label Aug 4, 2024
@eric-wieser
Copy link
Member Author

(edited the description with that justification)

@YaelDillies
Copy link
Collaborator

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Aug 4, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 5, 2024
@eric-wieser
refactor: use consistent names for forgetful smul structures (#15500)
4d93d88 
Moves:
- `AddCommMonoid.natModule` -> `AddCommMonoid.toNatModule`
- `AddCommGroup.intModule` -> `AddCommGroup.toIntModule`
- `algebraNat` -> `Semiring.toNatAlgebra`
- `algebraInt` -> `Ring.toIntAlgebra`
- `algebraRat` -> `DivisionRing.toRatAlgebra`
- `AddCommGroup.natModule.unique` -> `AddCommMonoid.uniqueNatModule`
- `AddCommGroup.intModule.unique` -> `AddCommGroup.uniqueIntModule`

The premise here is that the conversion from `AddCommGroup` to `AddCommMonoid` is not really any different from converting from `AddCommGroup` to `Module ℤ`; and so both should be named with the `to*` naming convention.

Tihs also brings the naming of the `Module` and `Algebra` instances into alignment.

I chose `toNatModule` instead of `toModuleNat` to match the prose, ℕ-module.
This fits a common naming convention if you view `Module` as infix, as we do with various other lean functions without actual infix notation.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Aug 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: use consistent names for forgetful smul structures [Merged by Bors] - refactor: use consistent names for forgetful smul structures Aug 5, 2024
@mathlib-bors mathlib-bors bot closed this Aug 5, 2024
@mathlib-bors mathlib-bors bot deleted the eric-wieser/rename-algebra-instances branch August 5, 2024 11:02
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@eric-wieser @bjoernkjoshanssen
refactor: use consistent names for forgetful smul structures (#15500)
39a780e 
Moves:
- `AddCommMonoid.natModule` -> `AddCommMonoid.toNatModule`
- `AddCommGroup.intModule` -> `AddCommGroup.toIntModule`
- `algebraNat` -> `Semiring.toNatAlgebra`
- `algebraInt` -> `Ring.toIntAlgebra`
- `algebraRat` -> `DivisionRing.toRatAlgebra`
- `AddCommGroup.natModule.unique` -> `AddCommMonoid.uniqueNatModule`
- `AddCommGroup.intModule.unique` -> `AddCommGroup.uniqueIntModule`

The premise here is that the conversion from `AddCommGroup` to `AddCommMonoid` is not really any different from converting from `AddCommGroup` to `Module ℤ`; and so both should be named with the `to*` naming convention.

Tihs also brings the naming of the `Module` and `Algebra` instances into alignment.

I chose `toNatModule` instead of `toModuleNat` to match the prose, ℕ-module.
This fits a common naming convention if you view `Module` as infix, as we do with various other lean functions without actual infix notation.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies Awaiting requested review from YaelDillies

Assignees
No one assigned
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@eric-wieser @YaelDillies @riccardobrasca