group element to the power of n

Stream: new members

[Saif Ghobash]

Hi all, I am unsure how to have something like (a)^n to denote a...a n times in lean where a is an element of a group and n is an natural number,

import algebra.group.basic
variables {α : Type*}  [comm_group α ]

-- Prove that if G is an abelian group, then for all a, b ∈ G
-- and all natural numbers  n, (a ⬝ b)^n = a^n ⬝ b^n
lemma ex2_3_2 :
 ∀ a b : α, ∀ n :ℕ, (a * b)^n = (a^n) * (b^n)  :=
begin
end

What I ended up doing was writing a function that performs group element exponentiation, I wanted to know is that if there is something like that in the library so I don't have to reprove any lemmas?

[Kevin Buzzard]

import algebra.group_power is what you're missing. There's plenty of API in there too.

[Kevin Buzzard]

I think the reason it's not there is that perhaps Lean uses groups to define the naturals or something? This trips a lot of people up.

[Saif Ghobash]

@Kevin Buzzard Oh perfect that's exactly what I needed, thank you!