Affine independent finset

Stream: Is there code for X?

[Yaël Dillies]

Where is the statement that the cardinality of an affine indpeendent finset is bounded by the dimension of the space + 1?

[Oliver Nash]

I'm not sure if we have this exact statement but it is certainly trivially implied by many of the results in affine_space/finite_dimensional.lean