Zulip Chat Archive

Stream: general

Topic: finite_dimensional performance issues

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: Dec 20 2023 at 11:08 UTC