mathlib3

35a16a94 - feat(algebra/module/basic): Add symmetric smul_comm_class instances for int and nat (#5369)

feat(algebra/module/basic): Add symmetric smul_comm_class instances for int and nat (#5369) These can't be added globally for all types as they cause instance resolution loops, but are safe here as these definitions do not depend on an existing `smul_comm_class`. Note that these instances already exist via `is_scalar_tower.to_smul_comm_class'` for algebras - this just makes sure the instances are still available in the presence of weaker typeclasses. There's no diamond concern here, as `smul_comm_class` is in `Prop`.