Zulip Chat Archive

Stream: general

Topic: deterministic craziness


view this post on Zulip Johan Commelin (Aug 28 2019 at 06:33):

Consider the following example:

import ring_theory.adjoin_root
import ring_theory.integral_closure

open algebra
variables {k : Type*} [discrete_field k]
variables {L : Type*} [discrete_field L] [algebra k L]
variables (L_alg :  x : L, is_integral k x)
variables (f : polynomial L) (hif : irreducible f)

instance : algebra L (adjoin_root f) :=
algebra.of_ring_hom coe $ by apply_instance

include L_alg --hif

lemma alg_trans (x : comap k L (adjoin_root f)) : is_integral k x :=
_

If you remove the -- in the include statement, you get a timeout.

view this post on Zulip Johan Commelin (Aug 28 2019 at 06:33):

I have zero understanding of why. Adding the assumption that f is irreducible seems completely harmless.

view this post on Zulip Johan Commelin (Aug 28 2019 at 06:35):

@Sebastian Ullrich Why can the mere adding of an assumption cause timeouts?

view this post on Zulip Chris Hughes (Aug 28 2019 at 06:36):

The instance saying adjoin_root is a field depends on irreducible f

view this post on Zulip Johan Commelin (Aug 28 2019 at 07:25):

But why would that matter?

view this post on Zulip Johan Commelin (Aug 28 2019 at 07:26):

I don't need that instance

view this post on Zulip Chris Hughes (Aug 28 2019 at 07:31):

You need a ring or comm_ring instance presumably, and that instance would provide a path.


Last updated: May 15 2021 at 02:11 UTC