Wrenna Robson (Apr 08 2022 at 17:19):
When I use the finite_dimensional definitions and lemmas in mathlib, even just in statements, they seem to work very slowly. Specifically I'm asserting things like finite_dimensional (degree_lt F t). It's honestly annoying enough that I think I'm going to have to find another way around it... anyone know what the cause might be?
Scott Morrison (Apr 08 2022 at 23:48):
Could you post a #mwe for people to have a look at?
Last updated: Aug 03 2023 at 10:10 UTC