affine_subspace): more `mem_map` lemmas (#16378)

Commit

3 years ago

feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378) Add two more lemmas about membership of an affine subspace given by `affine_subspace.map`.

Author

jsm28

Committer

b-mehta

Parents

5901b51c

mathlib3 d45bb4b4 - feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378)

mathlib3
d45bb4b4 - feat(linear_algebra/affine_space/affine_subspace): more `mem_map` lemmas (#16378)