Zulip Chat Archive
Stream: mathlib4
Topic: cache LinearAlgebra.Quotient
Yury G. Kudryashov (May 22 2023 at 14:16):
After lake exe cache get, Lean recompiles Mathlib.LinearAlgebra.Quotient (at least, on branch4#port/Analysis.Calculus.Fderiv.Bilinear)
Last updated: Dec 20 2023 at 11:08 UTC