mathlib

f1dfece4 - feat(linear_algebra/affine_space): bundled affine independent families (#3561)

feat(linear_algebra/affine_space): bundled affine independent families (#3561) Define `affine_space.simplex` as `n + 1` affine independent points, with the specific case of `affine_space.triangle`. I expect most definitions and results for these types (such as `circumcenter` and `circumradius`, which I'm currently working on) will be specific to the case of Euclidean affine spaces, but some make sense in a more general affine space context.