Commit 2026-10-21 15:52 80dabc7f
View on Github →chore: whitespace fixes (#45125) This PR fixes a small number of whitespace issues that the whitespace linter missed because of a bug in the Lean core pretty printer. The bug was fixed in https://github.com/leanprover/lean4/pull/15811, so starting from today's nightly, the whitespace linter finds them. The present PR backports the fixes from https://github.com/leanprover/downstream-lean4/pull/186 to mainline mathlib.