Commit 2022-06-15 03:13 38ad656e
View on Github →chore(field_theory/intermediate_field): fix timeout (#14725)
- Remove
@[simps]
fromintermediate_field_map
to reducedecl post-processing of intermediate_field_map
from 18.3s to 46.4ms (on my machine). - Manually provide the two
simp
lemmas previously auto-generated by@[simps]
. Mathlib compiles even without the two simp lemmas (see commit 1f5a7f1), but I am inclined to keep them in case some other branches/projects are using them. Zulip reports aboutintermediate_field_map
causing timeout in two separate branches