Commit 2024-07-21 10:19 08f062ac

View on Github →

chore: tidy various files (#14968)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Colimits.lean

modified inductive RingCat.Colimits.Prequotient

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Group/Action/Basic.lean

Modified Mathlib/Algebra/Lie/Weights/Cartan.lean

Modified Mathlib/Algebra/Module/Submodule/Localization.lean

Modified Mathlib/Algebra/Star/NonUnitalSubsemiring.lean

Modified Mathlib/Algebra/Tropical/BigOperators.lean

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

Modified Mathlib/CategoryTheory/Bicategory/Coherence.lean

Modified Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

Modified Mathlib/Combinatorics/Colex.lean

Modified Mathlib/Data/Nat/BitIndices.lean

Modified Mathlib/Data/Set/Constructions.lean

Modified Mathlib/Data/Set/Sups.lean

Modified Mathlib/Data/Sum/Order.lean

Modified Mathlib/Geometry/Manifold/InteriorBoundary.lean

Modified Mathlib/GroupTheory/Coset.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

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

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/NumberTheory/MulChar/Basic.lean

Modified Mathlib/NumberTheory/SiegelsLemma.lean

Modified Mathlib/Order/LiminfLimsup.lean

Modified Mathlib/Probability/Distributions/Exponential.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

Modified Mathlib/RingTheory/WittVector/Verschiebung.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

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

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Instances/Irrational.lean

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean