Commit 2025-11-24 20:05 90311041

View on Github →

chore: tidy various files (#31907)

Estimated changes

Modified Mathlib/Algebra/Lie/Extension.lean

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

Modified Mathlib/Algebra/QuadraticAlgebra/Basic.lean

modified theorem QuadraticAlgebra.norm_intCast

modified theorem QuadraticAlgebra.norm_natCast

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/Convex/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/Meromorphic/TrailingCoefficient.lean

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

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/ObjectProperty/ColimitsClosure.lean

Modified Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean

Modified Mathlib/CategoryTheory/Retract.lean

modified def CategoryTheory.RetractArrow.unop

Modified Mathlib/Combinatorics/Matroid/Closure.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hall.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/GroupTheory/Perm/MaximalSubgroups.lean

Modified Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Slope.lean

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

Modified Mathlib/NumberTheory/ZetaValues.lean

Modified Mathlib/Order/BourbakiWitt.lean

modified theorem ChainCompletePartialOrder.map_mem_bot

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Subsemiring.lean

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/Tactic/Simproc/FinsetInterval.lean

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