mathlib3

eae1ec81 - feat(analysis/normed/group/add_torsor): `normed_add_torsor` instance for `affine_subspace` (#16339)

feat(analysis/normed/group/add_torsor): `normed_add_torsor` instance for `affine_subspace` (#16339) Add an instance that a nonempty affine subspace of a `normed_add_torsor` is itself a `normed_add_torsor` (building on the existing instance that says such a subspace of an `add_torsor` is itself an `add_torsor`). Note that this instance uses `@[nolint fails_quickly]`, because of a typeclass loop with the `add_torsor.nonempty` instance. I don't know the right way to avoid that typeclass loop, but I don't think it's meaningfully a new issue, since exactly the same nolint appears in `nolints.txt` for `affine_subspace.to_add_torsor`.