Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Core Aleksandrov Jet Infrastructure #
The development lives in the Core/ submodules; this file re-exports all of
them.
Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
The development lives in the Core/ submodules; this file re-exports all of
them.