affine_subspace): affine_subspace.comap (#10795)

Commit

4 years ago

feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795) This copies a handful of lemmas from `group_theory/subgroup/basic.lean` to get things started.

Author

eric-wieser

Parents

00454f23

mathlib3 47c676ed - feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795)

mathlib3
47c676ed - feat(linear_algebra/affine_space/affine_subspace): affine_subspace.comap (#10795)