Maintainer merge (comment)

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

Sign in to view logs

Triggered via issue October 9, 2024 14:28

mathlib-bors[bot]

commented on #17576 b9cabbf

Status Skipped

Total duration 2s

Artifacts –

maintainer_merge_comment.yml

on: issue_comment

Ping maintainers on Zulip