More add_action instances

Stream: general

[Eric Wieser]

Do we want any of these instances?

-- this might need `add_monoid_with_one` to extend `has_vadd` to avoid diamonds
instance add_monoid_with_one.to_nat_add_action {A} [add_monoid_with_one A] : add_action ℕ A :=
{ vadd := λ n a, n + a,
  zero_vadd := λ n, by simp,
  add_vadd := λ n₁ n₂ a, by simp [add_assoc] }

instance add_group_with_one.to_int_add_action {A} [add_group_with_one A] : add_action ℤ A :=
{ vadd := λ z a, z + a,
  zero_vadd := λ z, by simp,
  add_vadd := λ z₁ z₂ a, by simp [add_assoc] }

instance {R} [add_monoid R] [add_action R ℝ] : add_action R ℂ :=
{ vadd := λ r z, ⟨r +ᵥ z.re, z.im⟩,
  zero_vadd := λ r, by simp,
  add_vadd := λ r₁ r₂ z, complex.ext (by simp [add_vadd]) rfl }

instance {R} [add_monoid R] [add_action R ℝ] : add_action R ℍ :=
{ vadd := λ r z, ⟨r +ᵥ z, by simpa [(+ᵥ)] using z.prop⟩,
  zero_vadd := λ r, by simp,
  add_vadd := λ r₁ r₂ z, subtype.ext (by simp [add_vadd]) }

[Eric Wieser]

Perhaps more ambitiously; we could makealgebra R A forgetfully decay to a add_action R A instance satisfyingr +ᵥ a = algebra_map R A r + a.

[Eric Wieser]

The motivation here was to be able to state docs#modular_group.coe_T_zpow_smul_eq without the coercion, as (T^n) • z = n +ᵥ z