Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
Restrictions to affine lines #
This module aggregates the split implementation files for the original public import path.
Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.
This module aggregates the split implementation files for the original public import path.