Commit 2025-04-07 04:49 e1a7a7f3

View on Github →

chore: tidy various files (#23665)

Estimated changes

Modified Archive/Sensitivity.lean

Modified Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Algebra/Order/Field/Power.lean

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

Modified Mathlib/Algebra/Order/WithTop/Untop0.lean

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

Modified Mathlib/Analysis/Meromorphic/Order.lean

Modified Mathlib/Analysis/Normed/Ring/Basic.lean

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

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

Modified Mathlib/Combinatorics/SimpleGraph/Diam.lean

Modified Mathlib/Data/ENat/Lattice.lean

Modified Mathlib/Data/Finset/Card.lean

modified theorem Finset.exists_mem_not_mem_of_card_lt_card

Modified Mathlib/Data/Finset/Preimage.lean

Modified Mathlib/Data/Finsupp/SMulWithZero.lean

Modified Mathlib/Data/LocallyFinsupp.lean

Modified Mathlib/Data/Matroid/Loop.lean

Modified Mathlib/Data/Matroid/Minor/Basic.lean

Modified Mathlib/Data/Matroid/Rank/Cardinal.lean

Modified Mathlib/Data/Matroid/Rank/ENat.lean

Modified Mathlib/Data/Nat/Cast/WithTop.lean

modified theorem Nat.cast_withTop

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

Modified Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

Modified Mathlib/MeasureTheory/Function/FactorsThrough.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasureExt.lean

Modified Mathlib/NumberTheory/SelbergSieve.lean

Modified Mathlib/Probability/ProductMeasure.lean

Modified Mathlib/RingTheory/MvPowerSeries/Evaluation.lean

Modified Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

modified theorem ContinuousLinearMap.coe_proj

Modified Mathlib/Topology/Basic.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean

Modified MathlibTest/positivity.lean