Zulip Chat Archive

Stream: new members

Topic: Fintype.card

Janitha Aswedige (Oct 12 2025 at 07:54):

I'm trying to formalize a group theory theorem.

theorem theorem_groups (G : Type*) [Group G] [Fintype G] (n : ℕ)
    (h : (Subgroup.center G).index = n) :
    ∀ (x : G), Fintype.card {y : G | IsConj x y} ≤ n := by

When I use Nat.card I don't get any errors. But I want to go with Fintype.card as I might want to apply the orbit stabilizer theorem. How do I fix it?

Kenny Lau (Oct 12 2025 at 07:58):

@Janitha looking at the error message is usually helpful.

Kenny Lau (Oct 12 2025 at 07:58):

in this case it is probably complaining about a lack of the needed Fintype instances

Kenny Lau (Oct 12 2025 at 07:59):

if the instances you need are for the statement, then you should add those instances to the assumption

Kenny Lau (Oct 12 2025 at 08:00):

if it's in the proof, then you provide those instances using Subtype.fintype and the classical tactic

Janitha Aswedige (Oct 12 2025 at 08:07):

@Kenny Lau The error message is for the statement of the theorem. When I replace Fintype.card with Nat.card, Lean doesn't complain.

Error:

failed to synthesize
Fintype { y // IsConj x y }

Kenny Lau (Oct 12 2025 at 08:08):

Janitha said:

When I replace Fintype.card with Nat.card, Lean doesn't complain.

yes, Nat.card can be applied to any type, but Fintype.card requires a fintype instance

Kenny Lau (Oct 12 2025 at 08:08):

so add [\forall x, Fintype { y // IsConj x y }] to your instance if you want to use Fintype.card in the statement

Kenny Lau (Oct 12 2025 at 08:10):

people might not realise this, but getting the statements right can be very difficult at first, it's much easier to start with a correctly formulated statement provided by someone else, and work out the proof yourself

Kenny Lau (Oct 12 2025 at 08:11):

I would advise you to actually not use the Fintype stuff in the statement

Kenny Lau (Oct 12 2025 at 08:11):

use Nat.card and replace the Fintype G assumption with Finite G.

Robin Arnez (Oct 12 2025 at 08:12):

With Nat.card and Finite in the statement, you can then start the proof with:

classical
have := Fintype.ofFinite G
simp only [Nat.card_eq_fintype_card]

to get it back to how you had it before

Janitha Aswedige (Oct 12 2025 at 08:13):

Thanks! That fixed it.

theorem theorem_groups (G : Type*) [Group G] [Fintype G] [∀ x : G, Fintype { y // IsConj x y }] (n : ℕ)
    (h : (Subgroup.center G).index = n):
    ∀ (x : G), Fintype.card {y : G // IsConj x y} ≤ n := by

If I use Nat.card and replaced the Fintype G assumption with Finite G, how would I use a theorem that uses Fintype.card in its statement?

Kenny Lau (Oct 12 2025 at 08:13):

read the message above you

Kenny Lau (Oct 12 2025 at 08:14):

basically, Lean needs to be guided in every way (as you probably know), and one of the things that is obvious to mathematicians but not to Lean is when things are finite