Commit 2024-12-03 10:57 1ec33a40

chore: cleanup set_option linter.deprecated (#19701) Remove several uses of deprecated lemmas in non-deprecated lemmas. Also convert all set_option linter.deprecated false to set_option linter.deprecated false in, so it is easier for us to count via regex what remains. I think

set_option linter\.deprecated false.*(?:(?:\n/--.*?-/\n(?!.*deprecated))|\n(?!.*deprecated|/--))

is the correct regex to use now: it accounts properly for intervening doc-strings. It now reports that there are only three one! files that use set_option linter.deprecated false on non-deprecated declarations, namely:

• Mathlib.Data.List.Permutation (fixed by moving some List theorems earlier)
• Mathlib.LinearAlgebra.CliffordAlgebra.Grading (replace AlgHom.map_zero with just map_zero; only costs 2000 heartbeats)
• Mathlib.SetTheory.Ordinal.Arithmetic (which is a mess)