Commit 2021-01-08 05:13 efdcab1a

refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654) These were named inconsistently, and lots of proof was duplicated. The name changes are largely making the API for nsmul consistent with the one for gsmul:

• For ℕ:
  • Replaces nat.smul_def : n • x = n •ℕ x with nsmul_def : n •ℕ x = n • x
  • Renames semimodule.nsmul_eq_smul : n •ℕ b = (n : R) • b to nsmul_eq_smul_cast
  • Removes semimodule.smul_eq_smul : n • b = (n : R) • b
  • Adds nsmul_eq_smul : n •ℕ b = n • b (this is different from nsmul_def as described in the docstring)
  • Renames the instances to be named more consistently and all live under add_comm_monoid.nat_*
• For ℤ:
  • Renames gsmul_eq_smul : n •ℤ x = n • x to gsmul_def
  • Renames module.gsmul_eq_smul : n •ℤ x = n • x to gsmul_eq_smul
  • Renames module.gsmul_eq_smul_cast to gsmul_eq_smul_cast
  • Renames the instances to be named more consistently and all live under add_comm_group.int_*