[Merged by Bors] - feat: expand API around LinearMap.index #274067
Triggered via issue
August 27, 2026 07:09
mathlib-bors[bot]
Status
Success
Total duration
7s
Artifacts
–
bot_fix_style.yaml
on: issue_comment
Fix style issues from lint
4s