Commit 2025-12-17 19:48 c7d1b5b9

View on Github →

chore: golf using grind and simp (#32968)

Estimated changes

Modified Mathlib/Algebra/Ring/Int/Parity.lean

modified theorem Int.even_sign_iff

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/Topology/Separation/Basic.lean