Commit 2024-11-20 09:38 2fb27be9

View on Github →

chore(Algebra/Module): further split Defs.lean (#18995) The goal is that we can define Module without depending on Units. The following moves out of Defs.lean are included in this PR:

  • Module structure over Nat and Int go to Module/NatInt.lean
  • Composition with RingHoms goes to Module/RingHom.lean
  • Results about units go to Module/Basic.lean

Estimated changes

added theorem Units.neg_smul
deleted theorem Int.smul_one_eq_cast
deleted theorem Nat.cast_smul_eq_nsmul
deleted theorem Nat.smul_one_eq_cast
deleted def RingHom.smulOneHom
deleted def RingHom.toModule
deleted theorem Units.neg_smul
deleted theorem map_natCast_smul
deleted theorem nat_smul_eq_nsmul
deleted theorem nsmul_eq_smul_cast
deleted theorem ofNat_smul_eq_nsmul
added theorem Int.smul_one_eq_cast
added theorem Nat.cast_smul_eq_nsmul
added theorem Nat.smul_one_eq_cast
added theorem map_natCast_smul
added theorem nat_smul_eq_nsmul
added theorem nsmul_eq_smul_cast
added theorem ofNat_smul_eq_nsmul
added def RingHom.toModule