Commit 2025-06-28 20:43 8287b8d2

View on Github →

chore: tidy various files (#26491)

Estimated changes

Modified Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

Modified Mathlib/Algebra/Group/Pi/Basic.lean

Modified Mathlib/Algebra/Polynomial/Taylor.lean

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

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Positive.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

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

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

Modified Mathlib/Analysis/NormedSpace/MStructure.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

Modified Mathlib/CategoryTheory/Preadditive/CommGrp_.lean

Modified Mathlib/Computability/Encoding.lean

modified theorem Computability.decode_encodeNat

modified theorem Computability.decode_encodeNum

modified theorem Computability.decode_encodePosNum

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

Modified Mathlib/NumberTheory/NumberField/CMField.lean

Modified Mathlib/Order/KonigLemma.lean

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

Modified Mathlib/RingTheory/Polynomial/GaussNorm.lean

Modified Mathlib/RingTheory/PowerSeries/GaussNorm.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

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

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean