Commit 2026-01-08 15:08 da0d686a

View on Github →

chore(Archive,Counterexamples): find whitespace (#33759) Found by extending the whitespace linter to proof bodies in #30658.

Estimated changes

Modified Archive/Examples/Eisenstein.lean

Modified Archive/Examples/Kuratowski.lean

Modified Archive/Imo/Imo1960Q2.lean

modified theorem Imo1960Q2.isGood_iff

Modified Archive/Imo/Imo1982Q1.lean

Modified Archive/Imo/Imo2001Q2.lean

Modified Archive/Imo/Imo2005Q4.lean

Modified Archive/Imo/Imo2006Q3.lean

Modified Archive/Imo/Imo2013Q1.lean

Modified Archive/Imo/Imo2019Q4.lean

Modified Archive/Imo/Imo2024Q3.lean

Modified Archive/Imo/Imo2024Q5.lean

Modified Archive/OxfordInvariants/Summer2021/Week3P1.lean

Modified Archive/Sensitivity.lean

modified theorem Sensitivity.f_image_g

modified theorem Sensitivity.g_apply

Modified Archive/Wiedijk100Theorems/AreaOfACircle.lean

Modified Archive/Wiedijk100Theorems/BuffonsNeedle.lean

Modified Archive/Wiedijk100Theorems/HeronsFormula.lean

Modified Counterexamples/AharoniKorman.lean

added theorem Hollom.forall₂

added theorem Hollom.forall₃

deleted theorem Hollom.«forall₂»

deleted theorem Hollom.«forall₃»

Modified Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

Modified Counterexamples/HomogeneousPrimeNotPrime.lean

Modified Counterexamples/TopologistsSineCurve.lean