Commit 2026-11-10 23:17 0097fc31
View on Github →chore(Util/Export): deprecate (#45357)
The file Mathlib.Util.Export defines an export format for Lean declarations. It is not documented, not tested, and seemingly not used. Nowadays, there is the alternative https://github.com/leanprover/lean4export. So, we deprecate this file.