Commit 2025-05-12 19:50 d00b35bf

View on Github →

chore: tidy various files (#24803)

Estimated changes

Modified Mathlib/Algebra/Exact.lean

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Analysis/Meromorphic/Basic.lean

modified theorem MeromorphicAt.prod

Modified Mathlib/Analysis/SpecialFunctions/Bernstein.lean

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean

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

Modified Mathlib/Combinatorics/SimpleGraph/Tutte.lean

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

Modified Mathlib/LinearAlgebra/Multilinear/Curry.lean

modified theorem MultilinearMap.currySum_add

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

modified theorem Real.circleAverage_eq_integral_add

Modified Mathlib/NumberTheory/NumberField/Ideal.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/SimpleRing/Congr.lean

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Modified Mathlib/Topology/CWComplex/Abstract/Basic.lean

Modified Mathlib/Topology/CWComplex/Classical/Basic.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/Path.lean

Modified Mathlib/Topology/Sets/Closeds.lean

Modified Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean