Commit 2024-07-22 10:51 a4d31242

View on Github →

chore: tidy various files (#15008)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Algebra/Homology/Embedding/Boundary.lean

Modified Mathlib/Algebra/Module/Opposites.lean

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

Modified Mathlib/Analysis/Calculus/LocalExtr/Basic.lean

Modified Mathlib/Analysis/Complex/Schwarz.lean

Modified Mathlib/Analysis/Convex/Uniform.lean

Modified Mathlib/Analysis/NormedSpace/MazurUlam.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

Modified Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Order.lean

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Control/Functor/Multivariate.lean

Modified Mathlib/Data/Int/Order/Units.lean

Modified Mathlib/Data/Nat/Choose/Sum.lean

Modified Mathlib/Data/Rat/Defs.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Order.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

Modified Mathlib/MeasureTheory/Function/UnifTight.lean

Modified Mathlib/MeasureTheory/Integral/Gamma.lean

Modified Mathlib/MeasureTheory/Integral/Pi.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/Tactic/MinImports.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/MetricSpace/Ultra/Basic.lean

modified theorem IsUltrametricDist.mem_ball_iff