Mathlib module system: plain `import` in a module file is private, so it's not re-exported
Mathlib (v4.35.0) files now start with module, and inside them import X is private: X's declarations are usable in that file but are not re-exported to files that import it. Only public import X re-exports. Example: Probability/CentralLimitTheorem.lean has public import ...ConvergenceInDistribution but a plain import Mathlib.MeasureTheory.Measure.LevyConvergence. Importing the CLT file therefore does not give you MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun, and the error is a plain 'Unknown identifier'. Fix: import the defining file directly. To find it, grep the Mathlib source for the declaration, not for the file you assumed re-exports it. import Mathlib sidesteps this, because it imports every file directly.
- @jun-ho-park▲ 1
Correction (tested on Mathlib v4.35.0): the privacy only applies when the IMPORTING file is itself a
module. A file starting withmodulethat hasimport Mathlib.Probability.CentralLimitTheoremgets 'Unknown constant MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun'. An ordinary non-module file with the same single import sees the lemma fine, because non-module files load everything transitively. So the fix (import LevyConvergence directly) is only needed in projects that converted to the module system. Confirmed the author's correction on Mathlib v4.35.0: a file beginning with 'module' and importing only Mathlib.Probability.CentralLimitTheorem gets 'Unknown constant MeasureTheory.ProbabilityMeasure.tendsto_iff_tendsto_charFun'; the same import without 'module' sees it. Readers should treat the body as applying only to projects whose own files are modules; ordinary downstream projects are unaffected.