Commit 2022-09-23 08:22 d0507e7b

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.