## Stream: new members

### Topic: defining power on groups

#### Jason KY. (Feb 26 2020 at 16:05):

Hi! I am trying to experiment a bit with groups and I am a bit confused about the following,

I have defined my powers as

-- definition of powers
@[simp] def group_pow_nat {G : Type} [group G] : G → ℕ → G
| g 0 := 1
| g (n + 1) := group_pow_nat g n * g
instance group_has_pow_nat {G : Type} [group G] : has_pow G ℕ := ⟨group_pow_nat⟩

@[simp] def group_pow {G : Type} [group G] : G → ℤ → G
| g (int.of_nat 0) := 1
| g (int.of_nat n) := group_pow_nat g n
| g -[1+ n] := group_pow_nat g⁻¹ (n + 1)
instance group_has_pow {G : Type} [group G] : has_pow G ℤ := ⟨group_pow⟩


Which seems to work as I want it to. So my question is how should I show the following

lemma pow_int_of_nat {g : G} {n : ℕ} : g ^ (int.of_nat n) = group_pow_nat g n := sorry


I thought rflwould work however it seems that is not the case.

#### Jason KY. (Feb 26 2020 at 16:07):

Btw I am using this definition as groups

class has_group_notation (G : Type) extends has_mul G, has_one G, has_inv G

-- definition of the group structure
class group (G : Type) extends has_group_notation G :=
(mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)


#### Reid Barton (Feb 26 2020 at 16:07):

You would at least need a pattern match on n into 0 and other because there is one in the definition of group_pow. But then the pattern match there is quite unnecessary, isn't it?

#### Reid Barton (Feb 26 2020 at 16:07):

i.e. just delete the first line of the definition of group_pow, and it looks okay

#### Jason KY. (Feb 26 2020 at 16:08):

Wow! That worked perfectly! Thanks

#### Jason KY. (Feb 27 2020 at 20:01):

Hi again!
Is there an easy way of solving this?

example (n : ℕ) : -[1+ n] + 1 = -[1+ (n - 1)] := sorry


#### Reid Barton (Feb 27 2020 at 20:08):

Well, it's not true

is it?

Wrong for n=0

Oh! Right

#### Scott Morrison (Feb 27 2020 at 20:48):

What happened to that automatic counter-example finder?

#### Scott Morrison (Feb 27 2020 at 21:10):

But if @Simon Hudon wants to PR slim_check to mathlib I'd use it. :-)

#### Simon Hudon (Feb 27 2020 at 21:12):

It's planned. I should have time to put on mathlib in a few weeks, I can do it then

#### Jason KY. (Mar 05 2020 at 19:19):

I am trying to define normal and central subgroups for a bundled subgroup and I am wondering whats the best way of doing it.
Is it better to define it as a class or should it be a prop?

This is how I've done it for now:

def center (G : Type) [group G] := {g : G | ∀ k : G, k * g = g * k}

class central_subgroup (K : subgroup G) :=
(center : ∀ k ∈ K, k ∈ mygroup.center G)


#### Kevin Buzzard (Mar 05 2020 at 19:21):

If you're bundling subgroups then center G should have type subgroup G rather than set G

#### Kevin Buzzard (Mar 05 2020 at 19:22):

But I don't know whether central_subgroup should be a predicate is_central or a class or another structure

#### Reid Barton (Mar 05 2020 at 21:55):

Class versus not depends on whether you want to use type class inference. I wouldn't want to use it here, but tastes differ.

#### Reid Barton (Mar 05 2020 at 21:56):

Structure versus just making a def that's a Prop doesn't make a big difference, you can think of the structure as introducing a little bit of abstraction

#### Reid Barton (Mar 05 2020 at 21:57):

The structure is pretty much a slightly more heavyweight way to do the same thing

#### Reid Barton (Mar 05 2020 at 21:57):

Note if you have a class/structure it will never be inferred as a Prop, so you would definitely want to add that

#### Reid Barton (Mar 05 2020 at 21:57):

I would tend to call it is_central

#### Jason KY. (Mar 05 2020 at 22:00):

Alright! I will make it a prop then, it'll be easier to work with! :)

#### Reid Barton (Mar 05 2020 at 22:05):

For normal subgroups there might be a specific reason to use a class, namely so that you can make the quotient a group. But another way to handle it is to bundle the subgroup + proof that it's normal and define the quotient by that.

Last updated: May 12 2021 at 22:15 UTC