Commit 2025-05-01 12:28 f4adaa2f

View on Github →

chore: whitespace still (#24501) Mostly whitespace changes found by the linter at #24465.

Estimated changes

Modified Archive/Imo/Imo2019Q4.lean

Modified Mathlib/GroupTheory/CoprodI.lean

modified inductive Monoid.CoprodI.Rel

Modified Mathlib/GroupTheory/PushoutI.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/NumberTheory/FactorisationProperties.lean

modified theorem Nat.Prime.deficient_pow

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

modified theorem NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply

Modified Mathlib/RingTheory/Binomial.lean

modified theorem Ring.descPochhammer_smeval_add

Modified Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

modified def Ideal.quotEquivPowQuotPowSucc

Modified Mathlib/RingTheory/LocalRing/Subring.lean

modified theorem IsLocalRing.of_subring

Modified Mathlib/RingTheory/Regular/RegularSequence.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

modified def TwoSidedIdeal.orderIsoIsTwoSided

Modified Mathlib/SetTheory/Surreal/Multiplication.lean

modified inductive Surreal.Multiplication.Args

Modified Mathlib/Tactic/FunProp/ContDiff.lean

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean