Commit 2024-05-18 15:22 06db9344

View on Github →

chore: tidy various files (#12999)

Estimated changes

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

Modified Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean

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

Modified Mathlib/Algebra/Module/FinitePresentation.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

modified def Polynomial.toLaurentAlg

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

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Monad/EquivMon.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Data/Array/ExtractLemmas.lean

modified theorem Array.extract_append_right

modified theorem Array.extract_eq_of_size_le_end

Modified Mathlib/Data/LazyList/Basic.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

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

Modified Mathlib/Probability/ProbabilityMassFunction/Monad.lean

Modified Mathlib/Probability/Variance.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Kaehler.lean

Modified Mathlib/RingTheory/Norm.lean

Modified Mathlib/RingTheory/Trace.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

modified theorem hasProd_prod_of_ne_finset_one

modified theorem multipliable_of_ne_finset_one

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

Modified Mathlib/Topology/Homotopy/HomotopyGroup.lean

Modified Mathlib/Topology/UniformSpace/Ascoli.lean

Modified Mathlib/Topology/UniformSpace/Completion.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean