mathlib3
38ad656e - chore(field_theory/intermediate_field): fix timeout (#14725)

Commit
3 years ago
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](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deterministic.20timeout/near/285792556) about `intermediate_field_map` causing timeout in two separate branches
Author
Parents
Loading