Commit 2025-08-29 20:40 c7b2d42b

View on Github →

feat: subsingleton ℕ and ℤ modules (#27638) Provide some instances AddCommMonoid.subsingletonNatModule and AddCommMonoid.subsingletonIntModule. Also move some of the theorems about ℕ and ℤ modules from Algebra/Module/End to Algebra/Module/NatInt.

Estimated changes

Modified Mathlib/Algebra/Algebra/Rat.lean

Modified Mathlib/Algebra/Module/End.lean

deleted def AddCommGroup.uniqueIntModule

deleted theorem Int.cast_smul_eq_zsmul

deleted theorem int_smul_eq_zsmul

deleted theorem map_intCast_smul

Modified Mathlib/Algebra/Module/NatInt.lean

added def AddCommGroup.uniqueIntModule

added theorem Int.cast_smul_eq_zsmul

added theorem int_smul_eq_zsmul

added theorem map_intCast_smul

modified theorem nat_smul_eq_nsmul

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/RingTheory/OreLocalization/Ring.lean