Casts as actions

Stream: Is there code for X?

[Yaël Dillies]

Are these hidden somewhere?

import data.rat.cast

namespace nat
variables {α : Type*} [add_monoid_with_one α]

instance : add_action ℕ α := add_action.comp_hom _ $ nat.cast_add_monoid_hom α

@[simp] lemma vadd_def (n : ℕ) (a : α) : n +ᵥ a = ↑n + a := rfl

end nat

namespace int
variables {α : Type*} [add_group_with_one α]

instance : add_action ℤ α := add_action.comp_hom _ $ int.cast_add_hom α

@[simp] lemma vadd_def (n : ℤ) (a : α) : n +ᵥ a = ↑n + a := rfl

end int

namespace rat
variables {α : Type*} [division_ring α] [char_zero α]

instance : add_action ℚ α := add_action.comp_hom _ $ (rat.cast_hom α).to_add_monoid_hom

@[simp] lemma vadd_def (q : ℚ) (a : α) : q +ᵥ a = ↑q + a := rfl

end rat

[Yaël Dillies]

Of course the corresponding mul_actions also hold.

[Eric Wieser]

The first one looks like add_action.comp_hom nat.cast_add_monoid_hom

[Eric Wieser]

docs#add_action.comp_hom

[Eric Wieser]

And the others in the obvious way

[Eric Wieser]

I think there's a high risk of non-defeq diamonds with those instances though, something to be careful of

[Yaël Dillies]

Golfed

[Yaël Dillies]

Time for a nvadd field to add_monoid_with_one? :rofl:

[Yaël Dillies]

At least this works

example : nat.add_action = add_monoid.to_add_action _ := rfl
example : int.add_action = add_monoid.to_add_action _ := rfl
example : rat.add_action = add_monoid.to_add_action _ := rfl

[Eric Wieser]

I'm more concerned about prod, pi, and complex

[Eric Wieser]

But maybe this instance is safe more generally for [algebra R A] : add_action R A