mathlib3

13e99c70 - feat(algebra,linear_algebra,ring_theory): more is_central_scalar instances (#11297)

feat(algebra,linear_algebra,ring_theory): more is_central_scalar instances (#11297) This provides new transitive scalar actions: * on `lie_submodule R L M` that match the actions on `submodule R M` * on quotients by `lie_submodule R L M` that match the actions on quotients by `submodule R M` The rest of the instances in this PR live in `Prop` so do not define any further actions. This also fixes some overly verbose instance names.