HomePhabricator

reduce dependencies of Ordered_Euclidean_Space; move more general material from…

Authored by immler.

Description

reduce dependencies of Ordered_Euclidean_Space; move more general material from Cartesian_Euclidean_Space

Details

Committed
immlerNov 4 2019, 11:18 PM
Parents
rISABELLE38bed2483e6a: proper message (amending 94442fce40a5);
Branches
Unknown
Tags
Unknown