Commit 2024-07-08 17:58 ed825b9d

View on Github →

chore: tidy various files (#14516)

Estimated changes

Modified Mathlib/Algebra/Order/Group/PosPart.lean

Modified Mathlib/Analysis/Convex/Segment.lean

Modified Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

modified def CategoryTheory.Adjunction.unitAsIsoOfIso

Modified Mathlib/Control/Basic.lean

Modified Mathlib/Control/Bitraversable/Instances.lean

Modified Mathlib/Control/EquivFunctor.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/Nat/Size.lean

Modified Mathlib/Data/Rat/Defs.lean

modified theorem Rat.divInt_neg_one_one

modified theorem Rat.divInt_one_one

Modified Mathlib/Data/Real/Basic.lean

Modified Mathlib/Data/Sym/Basic.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Basic.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/Order/PFilter.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/RingTheory/Ideal/Pointwise.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/PiTensorProduct.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/Basic.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/Tactic/CategoryTheory/MonoidalComp.lean

Modified Mathlib/Topology/Algebra/Valued/ValuedField.lean

modified def Valued.integer

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean

Modified Mathlib/Topology/CompactOpen.lean