Commit 2022-05-13 02:53 bd5914f6

perf(field_theory/primitive_element): declare auxiliary function noncomputable! (#14071) The declaration roots_of_min_poly_pi_type is computable and gets compiled by Lean. Unfortunately, compilation takes about 2-3s on my machine and times out under #11759 (with timeouts disabled, it takes about 11s on that branch). Since the parameters are all elements of noncomputable types and its only use is a noncomputable fintype instance, nobody will care if we explicitly make it computable, and it saves a lot of compilation time. See also this Zulip thread on noncomputable! fixing mysterious timeouts: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeout/near/278494746