## Stream: general

### Topic: Using type classes in definitions

#### Robert Maxton (Oct 31 2020 at 17:06):

So, I have a theorem:

theorem class_equation (G: Type*) [fin_group G]:
fintype.card G =
fintype.card (center G)
+ (∑ x in (conjugacy_classes G), fintype.card x) :=
sorry


and I have proofs that conjugacy_classes G coerces to a fintype, as are all sets in conjugacy_classes G. How do I tell Lean that those proofs exist, so I can use ∑ and fintype.card x in the statement of the theorem?

#### Johan Commelin (Oct 31 2020 at 17:08):

Do you have instance : fintype (conjugacy_classes G) somewhere?

#### Johan Commelin (Oct 31 2020 at 17:08):

I don't know what you mean by "coerces to a fintype"

#### Johan Commelin (Oct 31 2020 at 17:09):

Note that ∑ x in foo is summing over a finset, whereas ∑ x : foo is summing over a Type (and there must be an instance of fintype foo).

#### Johan Commelin (Oct 31 2020 at 17:11):

Note that there is also finset.card, if you are taking the cardinality of a finset.

#### Robert Maxton (Oct 31 2020 at 17:12):

Well, what I have is a proof that, under certain conditions, there exists an instance of fintype (conjugacy_classes G). I'm not entirely sure how to write a dependent instance like that; do I have to define a structure for it, maybe?

#### Robert Maxton (Oct 31 2020 at 17:20):

and by "coerces to a fintype" I just mean fintype ↥(conjugacy_classes G)

#### Kevin Buzzard (Oct 31 2020 at 17:21):

I don't understand the question. Are you asking how to make a term of that type, or saying you can make a term of that type?

#### Robert Maxton (Oct 31 2020 at 17:22):

I'm saying I can make a term of that type, but not always; so my ability to coherently state my theorem is conditional.

#### Robert Maxton (Oct 31 2020 at 17:22):

Which actually sounds pretty 'just make a dedicated structure'-ish to me, except that I seem to have accidentally gotten it working ...

#### Robert Maxton (Oct 31 2020 at 17:22):

but now I want to know why this works:

theorem class_equation (G: Type*) [fin_group G]:
fintype.card G =
fintype.card (center G)
+ (∑ s: ↥(conjugacy_classes G), fintype.card s) :=
begin
sorry
end


#### Johan Commelin (Oct 31 2020 at 17:28):

We can't answer that without more context.

#### Johan Commelin (Oct 31 2020 at 17:29):

You'll need to link to a file with more code.

#### Robert Maxton (Oct 31 2020 at 17:31):

that's an mwe lol

or almost

#### Robert Maxton (Oct 31 2020 at 17:31):

import group_theory.subgroup
import group_theory.group_action
import data.fintype.basic
import algebra.big_operators

open subgroup
open_locale big_operators
open_locale classical

class fin_group (G: Type*) extends group G, fintype G

def conjugacy_classes (G: Type*) [group G]: set (set G) :=
{ s | ∃ a:G, s = group.conjugates a }

def nontrivial_conjugacy_classes (G: Type*) [group G]: set (set G) :=
{ s ∈ conjugacy_classes G | nontrivial s }

theorem class_equation (G: Type*) [fin_group G]:
fintype.card G =
fintype.card (center G)
+ (∑ s: (nontrivial_conjugacy_classes G), fintype.card s) :=
begin
sorry
end


#### Robert Maxton (Oct 31 2020 at 17:31):

there, that's an mwe

#### Robert Maxton (Oct 31 2020 at 17:31):

I have no idea why this works and I'm vaguely suspicious it shouldn't

#### Johan Commelin (Oct 31 2020 at 17:33):

Lean knows that s : set X and [fintype X] implies [fintype s]

#### Johan Commelin (Oct 31 2020 at 17:33):

Are you using VS code?

#### Johan Commelin (Oct 31 2020 at 17:33):

If so, you can explore your statement with the widgets in the infoview.

#### Johan Commelin (Oct 31 2020 at 17:33):

Click on the \sum symbol, and then click on finset.univ

#### Johan Commelin (Oct 31 2020 at 17:34):

You'll see subtype.fintype show up in a pop-up window.

#### Kevin Buzzard (Oct 31 2020 at 17:34):

You put open_locale classical so now sanity prevails and everything which is obviously finite classically is known to be finite in lean

#### Johan Commelin (Oct 31 2020 at 17:35):

If you want it to break, add @[irreducible] before one of the defs.

#### Robert Maxton (Oct 31 2020 at 17:35):

@Kevin Buzzard ahh, okay. That would make sense. I had kind of gotten used to having it off

#### Robert Maxton (Oct 31 2020 at 17:36):

and yeah I've been wandering around my file in VS Code but wasn't really getting anywhere

#### Mario Carneiro (Oct 31 2020 at 17:46):

By the way, regarding your earlier question about proving that congugacy_classes is finite, you can express it as finset.image group.conjugates_finset finset.univ provided that G has decidable equality

#### Mario Carneiro (Oct 31 2020 at 17:47):

where group.conjugates_finset a is defined as finset.image (\lam g, g^-1 * a * g) finset.univ

Last updated: May 10 2021 at 00:31 UTC