defining power on groups

Stream: new members

[Jason KY.]

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.
Thanks in advance!

[Jason KY.]

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]

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]

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

[Jason KY.]

Wow! That worked perfectly! Thanks

[Jason KY.]

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

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

[Reid Barton]

Well, it's not true

[Reid Barton]

is it?

[Patrick Massot]

Wrong for n=0

[Jason KY.]

Oh! Right

[Scott Morrison]

What happened to that automatic counter-example finder?

[Alex J. Best]

https://github.com/cipher1024/slim_check or https://gitlab.binets.fr/pablo.le-henaff/nunchaku-lean ?

[Scott Morrison]

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

[Simon Hudon]

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

[Jason KY.]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

I would tend to call it is_central

[Jason KY.]

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

[Reid Barton]

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.