Commit 2025-10-26 14:28 849e6264

View on Github →

chore: tidy various files (#30919)

Estimated changes

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

Modified Mathlib/Algebra/Lie/Abelian.lean

Modified Mathlib/Algebra/Lie/Basic.lean

Modified Mathlib/Algebra/Lie/Character.lean

Modified Mathlib/Algebra/Lie/Weights/IsSimple.lean

Modified Mathlib/Algebra/Polynomial/RuleOfSigns.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NonDegenerateSimplices.lean

Modified Mathlib/Analysis/CStarAlgebra/Basic.lean

Modified Mathlib/Analysis/Complex/ValueDistribution/FirstMainTheorem.lean

Modified Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

Modified Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

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

Modified Mathlib/CategoryTheory/Limits/Presentation.lean

Modified Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/CategoryTheory/Types/Monomorphisms.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/GroupTheory/DivisibleHull.lean

Modified Mathlib/GroupTheory/Finiteness.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CMField.lean

Modified Mathlib/NumberTheory/NumberField/Norm.lean

modified theorem RingOfIntegers.algebraMap_norm_algebraMap

Modified Mathlib/NumberTheory/SumTwoSquares.lean

Modified Mathlib/Probability/Distributions/Beta.lean

Modified Mathlib/Probability/Distributions/Gaussian/Basic.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean

Modified Mathlib/RingTheory/DividedPowers/Padic.lean

Modified Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Modified Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean