Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(analysis/normed_space/affine_isometry):
subtypeₐᵢ
(#16573)
Now that we have `affine_subspace.subtype`, add the corresponding definition as a bundled affine isometry (so resolving a comment about that being missing). The name uses subscript `ₐᵢ` rather than superscript `ᵃⁱ` as in the notation for `affine_isometry` because Lean does not accept the superscript in identifiers.
- Loading branch information