Zulip Chat Archive

Stream: new members

Topic: powers in semigroups?


view this post on Zulip Damiano Testa (Feb 21 2021 at 12:30):

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 ℕ
-/

view this post on Zulip Damiano Testa (Feb 21 2021 at 12:31):

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

view this post on Zulip Damiano Testa (Feb 21 2021 at 12:32):

Ok, this works:

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

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 14:05):

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

view this post on Zulip Damiano Testa (Feb 21 2021 at 15:08):

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!


Last updated: May 09 2021 at 20:11 UTC