Commit 2023-01-18 17:47 df78eae5

refactor(geometry/euclidean/angle/unoriented/basic): split out conformal map lemmas (#18210) Move two lemmas about conformal maps preserving angles to a separate geometry.euclidean.angle.unoriented.conformal, so eliminating the dependence of angles on calculus (and use assert_not_exists to declare that the basic file should not depend on calculus or conformal maps). None of the other Euclidean geometry results depend on these two lemmas.