Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-02 20:28 51696a64

View on Github →

chore(data/analysis/*): Fix lint and docs (#16751) Write the missing docstrings and module docs for data.analysis.filter and data.analysis.topology. Satisfy the has_nonempty_instance and unused_arguments linters.

Estimated changes