feat: check that every file imports Mathlib.Init

[grunweg]

We add a text-based check to the lint-style script, that every file either (transivively) imports Mathlib.Init, or is (transitively) imported by it.

---

[github-actions]

PR summary bebfe32f0e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ checkInitImports

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[bryangingechen]

Right now the module doc of Mathlib.Init says something like "this file is imported by virtually every file in Mathlib". If we add this linter, perhaps we should update that text and also mention that it's enforced by litner.

[grunweg]

Good point, updated the doc-string!