Commit 2022-10-13 20:27 1e9b3df5

View on Github →

refactor(geometry/euclidean/basic): rename cospherical_subset (#16947) Rename cospherical_subset to cospherical.subset to allow use of dot notation.

Estimated changes

Modified src/geometry/euclidean/basic.lean

added theorem euclidean_geometry.cospherical.subset

deleted theorem euclidean_geometry.cospherical_subset