Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 03:13 38ad656e

View on Github →

chore(field_theory/intermediate_field): fix timeout (#14725)

  • Remove @[simps] from intermediate_field_map to reduce decl 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 about intermediate_field_map causing timeout in two separate branches

Estimated changes