mathlib

bd5914f6 - perf(field_theory/primitive_element): declare auxiliary function `noncomputable!` (#14071)

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