gal of cyclotomic polynomial

Stream: maths

[Eric Rodriguez]

Hey all, I'm trying to work on the Galois group of cyclotomic polynomials. However, I'm stuck at the starting block; just defining the damn thing causes a deterministic timeout:

import field_theory.polynomial_galois_group
import ring_theory.polynomial.cyclotomic

open polynomial

variables {F : Type*} [field F] (n : ℕ)

noncomputable def cyclotomic_gal_hom : (cyclotomic n F).gal →* units (zmod n) := sorry
--timeout

anyone have any clue what I'm doing wrong, or how to get around it?

[Johan Commelin]

This is instant:

lemma cyclotomic_gal_hom : (cyclotomic n F).gal →* units (zmod n) := _

so there is something silly going on with elaboration

[Eric Rodriguez]

even specializing to ℚ doesn't lead anywhere :/ how do we usually get around elaboration issues like these?

[Johan Commelin]

Once you have filled in the definition, switching back from lemma to def usually works

[Johan Commelin]

It's a bit annoying...

[Eric Rodriguez]

yikes, I'll try that though and hopefully no more issues

[Johan Commelin]

it might be that Lean is trying to figure out whether you correctly marked the def as noncomputable

[Johan Commelin]

and that is taking a long time. But it should just give up, because of the sorry

[Johan Commelin]

But I'm just guessing...

[Kevin Buzzard]

I think Johan is right but this is really hard to minimise (i.e. get an example which is independent of mathlib)

[Riccardo Brasca]

I don't if this is relevant, but maybe the definition of cyclotomic polynomial should be irreducible, or something like that (all the basic properties are in the API, but the definition is rather unnatural, using cyclotomic').