Commit 2025-03-19 17:05 f6809bd5

View on Github →

chore: tidy various files (#23093)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Algebra/Group/Units/Defs.lean

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

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

Modified Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Modified Mathlib/Analysis/Normed/Group/Quotient.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart/Isometric.lean

Modified Mathlib/CategoryTheory/Sums/Basic.lean

Modified Mathlib/Computability/Language.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/ENat/Basic.lean

Modified Mathlib/Data/Finset/CastCard.lean

modified theorem Finset.cast_card_erase_of_mem

modified theorem Finset.cast_card_inter

modified theorem Finset.cast_card_sdiff

modified theorem Finset.cast_card_union

Modified Mathlib/Data/Finset/Pi.lean

Modified Mathlib/Data/List/Shortlex.lean

Modified Mathlib/FieldTheory/Finite/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/FreeModule/Finite/Quotient.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

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

Modified Mathlib/Order/CompleteLattice/Basic.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/HahnSeries/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/HahnSeries/PowerSeries.lean

Modified Mathlib/RingTheory/Ideal/Height.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/RingTheory/WittVector/IsPoly.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

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

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

Modified Mathlib/Topology/ContinuousMap/StarOrdered.lean

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