mathlib

d25f4d64 - feat(linear_algebra/affine_space/affine_subspace): `vadd_mem_iff_mem_of_mem_direction` (#16383)

feat(linear_algebra/affine_space/affine_subspace): `vadd_mem_iff_mem_of_mem_direction` (#16383) Add a lemma similar to `vadd_mem_iff_mem_direction`, but where it's given that the vector is in `s.direction` and the `iff` is between the two points being in the subspace.