Commit 2022-06-15 03:13 38ad656e
View on Github →chore(field_theory/intermediate_field): fix timeout (#14725)
- Remove
@[simps]fromintermediate_field_mapto reducedecl post-processing of intermediate_field_mapfrom 18.3s to 46.4ms (on my machine). - Manually provide the two
simplemmas 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_mapcausing timeout in two separate branches