Commit 2023-11-17 16:12 92bfd3b2

View on Github →

fix(LinearAlgebra/AffineSpace/Independent): fix case of Simplex.Independent (#8419) This holds a proof not a Prop, so should be lowercase.

Estimated changes

Modified Mathlib/Analysis/Convex/Between.lean

Modified Mathlib/Geometry/Euclidean/Angle/Sphere.lean

Modified Mathlib/Geometry/Euclidean/Circumcenter.lean

Modified Mathlib/Geometry/Euclidean/MongePoint.lean

Modified Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified scripts/nolints.json