Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have added also the statement of the two relative versions of the Serre spectral sequence (here). No details yet.
added this pointer:
and implementation in Lean is in
and will add it also to spectral sequence and maybe elsewhere
@Urs it should be Floris et. al. There is a list of participents:
Participants Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead, Egbert Rijke, Mike Shulman.
Checking the contributors supports this fact too.
all right, I added more of these names. I got the pointer from Floris’ talk at LeanTogether and somehow thought it was the pointer to his
In your proof, where it says’
we have for the given finite subgroup of SU(2) (by this Prop) that:
do you mean to give rather than ? Otherwise I don’t know what the parameter on the RHS of the equation is meant to be.
1 to 8 of 8