mathlib

273986ad - fix(topology/algebra/group_completion): add lemmas about nsmul and zsmul and fix diamonds (#14846)

fix(topology/algebra/group_completion): add lemmas about nsmul and zsmul and fix diamonds (#14846) This prevents a diamond forming between `uniform_space.completion.has_scalar` and the default `add_monoid.nsmul` and `sub_neg_monoid.zsmul` fields; by manually defining the latter to match the former. To do this, we add two new instances of `has_uniform_continuous_smul` for nat- and int- actions. To use the existing scalar actions, we had to shuffle the imports around a bit.