## Stream: maths

### Topic: make an explicit group

#### Kevin Buzzard (Jul 14 2020 at 21:28):

import tactic

inductive mu2
| p1 : mu2
| m1 : mu2

namespace mu2

def mul : mu2 → mu2 → mu2
| p1 p1 := p1
| p1 m1 := m1
| m1 p1 := m1
| m1 m1 := p1

def one : mu2 := p1

def inv : mu2 → mu2 := id

instance : group mu2 := dec_trivial -- doesn't work yet

end mu2


Is it easy to get this working automatically somehow?

#### Reid Barton (Jul 14 2020 at 21:48):

import tactic

@[derive decidable_eq] inductive mu2
| p1 : mu2
| m1 : mu2

instance : fintype mu2 := ⟨⟨[mu2.p1, mu2.m1], by simp⟩, λ x, by cases x; simp⟩

namespace mu2

def mul : mu2 → mu2 → mu2
| p1 p1 := p1
| p1 m1 := m1
| m1 p1 := m1
| m1 m1 := p1

def one : mu2 := p1

def inv : mu2 → mu2 := id

instance : group mu2 :=
by refine_struct { one := one, mul := mul, inv := inv }; exact dec_trivial

end mu2


Thanks!

#### Kevin Buzzard (Jul 14 2020 at 22:07):

I did all of that myself apart from the fintype, which I also tried to derive. I don't understand why we have to derive decidable equality, whereas if we want an extensionality lemma we just [ext]

#### Kevin Buzzard (Jul 14 2020 at 22:08):

Isn't there a way to derive the fintype instance?

#### Kyle Miller (Jul 14 2020 at 22:11):

Adding to that question, is there a list of all the derivable instances somewhere?

#### Reid Barton (Jul 14 2020 at 22:15):

Kevin Buzzard said:

Isn't there a way to derive the fintype instance?

You'd think so but afaik it isn't implemented.

Last updated: May 11 2021 at 15:12 UTC