mathlib

bd7af8ef - reframe line additivity to lower dimension