Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-21 08:15 e2ce3fa0

View on Github →

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.

Estimated changes