Zulip Chat Archive

Stream: new members

Topic: group element to the power of n


view this post on Zulip Saif Ghobash (Jan 27 2021 at 21:18):

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?

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 21:19):

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

view this post on Zulip Kevin Buzzard (Jan 27 2021 at 21:19):

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.

view this post on Zulip Saif Ghobash (Jan 27 2021 at 21:20):

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


Last updated: May 13 2021 at 22:15 UTC