Commit 2025-03-18 15:10 f1a5be53

feat: linter for bare open (scoped) Classical (#21947) Add a syntax linter for open Classical and open scoped Classical which are not scoped to a single declaration. Such occurrences have been tracked as technical debt, and recently been fully removed from mathlib. This linter enforces this (and removes the corresponding technical debt metric).