mathlib

efdcab1a - refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)

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_*`