Commit 2024-08-05 10:13 4d93d88d

refactor: use consistent names for forgetful smul structures (#15500) 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.