Commit 2025-06-17 18:33 1e3fd2ae

feat: a linter to enforce formatting (#24465) This linter enforces that the hypotheses of every declaration are correctly formatted. This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib.