mathlib

46c35cc1 - fix(algebra/module/basic): Do not attach the ℕ and ℤ `is_scalar_tower` and `smul_comm_class` instances to a specific definition of smul (#5509)

fix(algebra/module/basic): Do not attach the ℕ and ℤ `is_scalar_tower` and `smul_comm_class` instances to a specific definition of smul (#5509) These instances are in `Prop`, so the more the merrier. Without this change, these instances are not available for alternative ℤ-module definitions. An example of one of these alternate definitions is `linear_map.semimodule`, which provide a second non-defeq ℤ-module structure alongside `add_comm_group.int_module`. With this PR, both semimodule structures are shown to satisfy `smul_comm_class` and `is_scalar_tower`; while before it, only `add_comm_group.int_module` was shown to satisfy these. This PR makes the following work: ```lean example {R : Type*} {M₁ M₂ M₃ : Type*} [comm_semiring R] [add_comm_monoid M₁] [semimodule R M₁] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃] (f : M₁ →ₗ[R] M₂ →ₗ[R] M₃) (x : M₁) (n : ℕ) : f (n • x) = n • f x := by simp ```