Commit 2024-12-20 12:30 83450e8f

View on Github →

chore: tidy various files (#17342)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Group/Aut.lean

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

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

Modified Mathlib/Algebra/Ring/Aut.lean

Modified Mathlib/Algebra/Ring/Subring/IntPolynomial.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Matrix/RowCol.lean

modified theorem Matrix.row_mulVec_eq_const

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

Modified Mathlib/Data/Nat/Defs.lean

Modified Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean

Modified Mathlib/FieldTheory/Adjoin.lean

deleted theorem IntermediateField.finrank_bot

deleted theorem IntermediateField.rank_bot

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

Modified Mathlib/GroupTheory/Perm/Finite.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace.lean

Modified Mathlib/LinearAlgebra/Vandermonde.lean

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

Modified Mathlib/NumberTheory/VonMangoldt.lean

Modified Mathlib/Order/Defs/LinearOrder.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/Order/RelClasses.lean

Modified Mathlib/RingTheory/Norm/Basic.lean

Modified Mathlib/RingTheory/Presentation.lean

Modified Mathlib/Topology/Order/ScottTopology.lean