Commit 2025-03-10 05:37 0d1fc218
View on Github →style: fix some isolated where's (#22726)
Mathlib style is to have the where on the previous line: there is even a linter meant to enforce this.
style: fix some isolated where's (#22726)
Mathlib style is to have the where on the previous line: there is even a linter meant to enforce this.