timeout at `whnf`, maximum number of heartbeats

Stream: new members

[Snir Broshi]

I tried to use docs#minpoly.eq_of_irreducible_of_monic and got a weird error:

import Mathlib.Data.Real.Basic
import Mathlib.FieldTheory.Minpoly.Field

open Polynomial

def h : Polynomial.aeval (0 : ℝ) (X : ℤ[X]) = 0 := by simp
def h' := @minpoly.eq_of_irreducible_of_monic ℤ ℝ _ _ _ 0 _ X irreducible_X h monic_X

Lean marks an error at the usage of h in h':
(deterministic) timeout at whnf, maximum number of heartbeats (200000) has been reached

I expected the error to be that it can't synthesize Field ℤ (btw i'm not sure why that theorem requires this), what happened?

Thanks!

[Ruben Van de Velde]

Yeah, if you start removing arguments from the end, the error changes to "failed to synthesize" as soon as you remove the h

[Ruben Van de Velde]

So lean is trying to unify the argument with your h and gets lost. Possibly for the same reason, maybe for another

[Damiano Testa]

With respect to the Field assumption, maybe it could be weakened to having no zero-divisors. However, $B = \mathbb{Z}/p$ is an $A = \mathbb{Z}/p^2$ algebra, the polynomial $x-p$ vanishes on 0 modulo p, and yet $x-p$ is not a minimal polynomial of 0 in A.

[Damiano Testa]

Actually, the example above may even work with $A = \mathbb{Z}$. I wonder if the "correct" assumption is that the algebra map $A \to B$ be injective.