affine_subspace): `mem_mk'_iff_vsub_mem` (#17524)

Commit

3 years ago

feat(linear_algebra/affine_space/affine_subspace): `mem_mk'_iff_vsub_mem` (#17524) Add another lemma about membership of `affine_subspace.mk'`.

Author

jsm28

Parents