Commit 2023-02-17 15:56 0324bd3f

fix(ring_theory/derivation): speed up a slow definition (#18457) 16s to 3s. I don't know which of the changes is responsible for the speedup, but they all seem sensible anyway. With the explicit to_fun field, we may as well use simps to generate a lemma for us.