Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 19:07 1068fdd9

View on Github →

feat(geometry/euclidean/basic): cospherical.affine_independent variants (#17645) Add some variants of cospherical.affine_independent that are more convenient in some cases than the version with an injective hypothesis.

Estimated changes