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: May 02 2025 at 03:31 UTC