mathlib3

b898874f - feat(linear_algebra/affine_space/affine_subspace): `affine_subspace.subtype` (#16372)

feat(linear_algebra/affine_space/affine_subspace): `affine_subspace.subtype` (#16372) Define `affine_subspace.subtype`, the embedding map from an affine subspace to the ambient affine space as a bundled affine map, analogous to `submodule.subtype`.