[Merged by Bors] - feat: `InnerProductSpace (SeparationQuotient E)` #702

	name: Autolabel PRs

	on:
	pull_request:
	types: [opened]
	push:
	paths:
	- scripts/autolabel.lean
	- .github/workflows/add_label_from_diff.yaml

	jobs:
	add_topic_label:
	name: Add topic label
	runs-on: ubuntu-latest
	# Don't run on forks, where we wouldn't have permissions to add the label anyway.
	if: github.repository == 'leanprover-community/mathlib4'
	permissions:
	issues: write
	checks: write
	pull-requests: write
	contents: read
	steps:
	- name: Checkout code
	uses: actions/checkout@v4
	with:
	fetch-depth: 0
	- name: install elan
	run: \|
	set -o pipefail
	curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz \| tar xz
	./elan-init -y --default-toolchain none
	echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
	- name: lake exe autolabel
	run: \|
	# the checkout dance, to avoid a detached head
	git checkout master
	git checkout -
	lake exe autolabel "$NUMBER"
	env:
	GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	GH_REPO: ${{ github.repository }}
	NUMBER: ${{ github.event.number }}

Provide feedback