Commit 2026-06-03 21:39 1450d19e

View on Github →

chore: remove most warning.simp.varHead (#40111) This pr removes most exceptions to the new simpVar linter.

Estimated changes

Modified Archive/Examples/IfNormalization/Result.lean

Modified Archive/Imo/Imo2024Q6.lean

Modified Mathlib/Algebra/CharP/Two.lean

modified theorem CharTwo.ofNat_eq_mod

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

Modified Mathlib/Probability/Kernel/Defs.lean