Commit 2025-12-27 16:28 c05a1aed

View on Github →

chore: tidy various files (#33340)

Estimated changes

Modified Counterexamples/NowhereDifferentiable.lean

modified theorem NowhereDifferentiable.seq_le

Modified Mathlib/Algebra/AffineMonoid/Basic.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

modified theorem IsLocalizedModule.map_id

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/Algebra/Order/Floor/Semifield.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/CategoryTheory/Functor/Derived/PointwiseLeftDerived.lean

Modified Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

Modified Mathlib/Combinatorics/SetFamily/Compression/Down.lean

Modified Mathlib/Combinatorics/SimpleGraph/Matching.lean

Modified Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Geometry/Convex/Cone/Basic.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean

Modified Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean

Modified Mathlib/Geometry/Euclidean/Triangle.lean

Modified Mathlib/GroupTheory/QuotientGroup/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

Modified Mathlib/LinearAlgebra/Transvection.lean

Modified Mathlib/MeasureTheory/Measure/Tight.lean

Modified Mathlib/NumberTheory/NumberField/House.lean

modified theorem NumberField.house_nat_mul

modified theorem NumberField.house_pow_le

Modified Mathlib/Probability/Distributions/Gaussian/Real.lean

Modified Mathlib/Probability/Distributions/SetBernoulli.lean

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/FiniteCyclic.lean

Modified Mathlib/Topology/Algebra/UniformField.lean