powers in semigroups?

Stream: new members

[Damiano Testa]

Dear All,

should I do something special in order to "activate" the notation ^ for semigroups? What is below is an example of the kind of thing that I would like.

Thanks!

import algebra.group_power.basic

example {R : Type*} [semigroup R] {a : R} : a ^ 1 = a := sorry
/- failed to synthesize type class instance for
R : Type ?,
_inst_1 : semigroup R,
a : R
⊢ has_pow R ℕ
-/

[Damiano Testa]

Ah, maybe the issue is that a ^ 0 does not make sense if there is no assumption of 1 : R?

[Damiano Testa]

Ok, this works:

example {R : Type*} [monoid R] {a : R} : a ^ 1 = a :=
begin
  apply pow_one,
end

[Kevin Buzzard]

You could make a has_pow S pnat instance for semigroups :-)

[Damiano Testa]

Is this something that people would want? I am happy to do it, even if it is just to learn how induction works on pnat!