AddGroup for Fin

Stream: mathlib4

[Daniel Weber]

Is there a reason there's no AddGroup (I actually need AddGroupWithOne) instance for Fin? I want to apply docs#Nat.cast_sub but I can't

[Kevin Buzzard]

Fin 0 isn't a group

[Kevin Buzzard]

I can recommend ZMod n

[Kevin Buzzard]

Or Fin (n+1) if you are convinced it's Fin you want even though you want a group structure

[Daniel Weber]

It is a concrete Fin 31, but there's no AddGroup instance for it

[Daniel Weber]

Is there anything convenient to convert from Fin to ZMod and vice versa? I get my input as Fin, so if I want to use ZMod I'll have to convert to it

[Yaël Dillies]

Daniel Weber said:

It is a concrete Fin 31, but there's no AddGroup instance for it

Try adding NeZero 31 to your context

[Yaël Dillies]

Daniel Weber said:

Is there anything convenient to convert from Fin to ZMod and vice versa? I get my input as Fin, so if I want to use ZMod I'll have to convert to it

ZMod 31 is defined as Fin 31 (and all operations agree

[Daniel Weber]

Wouldn't using that be defeq abuse?

[Kevin Buzzard]

You can't call a definition defeq abuse surely

[Daniel Weber]

Oh, I see there's docs#Fin.instCommRing, but I didn't find it because I was missing the import and loogling for AddGroup, Fin doesn't find it :man_facepalming:

[Kevin Buzzard]

Yeah this is an annoying consequence of the current "minimise imports" culture, it also minimises the chance that you've got the correct stuff imported to actually prove what you've just stated