# Zulip Chat Archive

## Stream: maths

### Topic: integral domain timeout

#### Kevin Buzzard (Jan 17 2020 at 17:26):

Can others reproduce this:

import data.mv_polynomial import ring_theory.ideal_operations open mv_polynomial variables {k : Type*} [comm_ring k] variable {n : Type*} def 𝕍 (S : set (mv_polynomial n k)) : set (n → k) := {x : n → k | ∀ f ∈ S, eval x f = 0} -- works BUT VARIABLES IN STUPID ORDER! set_option profiler true -- typechecks in under a second theorem 𝕍_radical {k : Type*} [comm_ring k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry -- (deterministic) timeout theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

#### Kevin Buzzard (Jan 17 2020 at 17:32):

-- works fine noncomputable instance {k : Type*} [integral_domain k] {n : Type*} : has_coe (ideal (mv_polynomial n k)) (set (mv_polynomial n k)) := by apply_instance -- times out noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

#### Kevin Buzzard (Jan 17 2020 at 17:35):

-- times out noncomputable theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (I : set (mv_polynomial n k)) = 𝕍 ((ideal.radical I : ideal _) : set _) := sorry

#### Kevin Buzzard (Jan 17 2020 at 17:36):

-- works theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (↑I : set (mv_polynomial n k)) = 𝕍 (↑(ideal.radical I : ideal _) : set _) := sorry

So when do I need the up-arrows?

#### Kevin Buzzard (Jan 17 2020 at 17:37):

And why did I not need them for comm_rings?

#### Kevin Buzzard (Jan 17 2020 at 17:40):

theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (↑I : set _) = 𝕍 (↑(ideal.radical I) : set _) := sorry -- don't know how to synthesize placeholder

gaargh

#### Kevin Buzzard (Jan 17 2020 at 17:41):

why does it look so ugly?

#### Kevin Buzzard (Jan 17 2020 at 17:41):

I am trying to sell this software to mathematicians

#### Johan Commelin (Jan 17 2020 at 17:47):

I guess that you can play tricks, if you want. Where you make `k \^n`

notation for `fin n → k`

, similar to the way that Mario made the `\bbV`

notation. Idem dito for `k[X_1, ..., X_n]`

.

#### Johan Commelin (Jan 17 2020 at 17:47):

But such hacks will likely break down fast

#### Kevin Buzzard (Jan 17 2020 at 18:05):

Will Lean 4 be better in this regard?

#### Andrew Ashworth (Jan 17 2020 at 19:50):

Do you need to have the displayed content equal to the keystrokes you type in? If not, then the VSCode plugin - if it was extended appropriately - could probably render formulas to latex

#### Kevin Buzzard (Jan 17 2020 at 20:01):

No I definitely don't need this. @Patrick Massot can hacking VSCode give me $k^n$ instead of `fin n -> k`

?

#### Daniel Selsam (Jan 17 2020 at 20:07):

Can others reproduce this:

-- (deterministic) timeout theorem 𝕍_radical' {k : Type*} [integral_domain k] {n : Type*} (I : ideal (mv_polynomial n k)) : 𝕍 (I : set (mv_polynomial n k)) = 𝕍 (I.radical) := sorry

Diamonds. Two searches for `has_coe_to_fun`

traverse `discrete_linear_ordered_field`

14,000x times each.

#### Kevin Buzzard (Jan 17 2020 at 20:08):

Daniel thank you so much for these advanced debugging comments. I am just writing MSc level mathematics in a mathematically normal way and coming up with these issues in Lean 3, I am quite excited about Lean 4 now.

Last updated: May 06 2021 at 18:20 UTC