Commit 2023-03-16 11:15 eea141bc

View on Github →

refactor(geometry/euclidean): split out spheres (#18220) Rearrange material related to spheres as follows:

  • geometry.euclidean.sphere.power has most of the content from the previous geometry.euclidean.sphere (intersecting chords / secants, which at some point should probably be refactored using an explicit definition of the power of a point).
  • geometry.euclidean.sphere.ptolemy has the proof of Ptolemy's theorem that was previously in geometry.euclidean.sphere.
  • geometry.euclidean.sphere.basic has most of the material previously in geometry.euclidean.basic: definitions of sphere, cospherical and concyclic and associated lemmas.
  • geometry.euclidean.sphere.second_inter has the definition and lemmas about second_inter. There are no changes to API or proofs.

Estimated changes

deleted structure euclidean_geometry.concyclic
deleted structure euclidean_geometry.sphere
added structure euclidean_geometry.sphere