Commit 2023-06-27 00:20 0e36dc3b

View on Github →

chore: tidy various files (#5482)

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

deleted theorem AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_to_Γ_Spec

added theorem AlgebraicGeometry.LocallyRingedSpace.toStalk_stalkMap_toΓSpec

deleted theorem AlgebraicGeometry.LocallyRingedSpace.to_Γ_Spec_continuous

deleted theorem AlgebraicGeometry.LocallyRingedSpace.to_Γ_Spec_preim_basicOpen_eq

added theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous

added theorem AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preim_basicOpen_eq

Modified Mathlib/AlgebraicGeometry/PresheafedSpace/Gluing.lean

Modified Mathlib/Analysis/Complex/Schwarz.lean

Modified Mathlib/Analysis/ODE/PicardLindelof.lean

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

Modified Mathlib/Data/Real/Pi/Bounds.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMap.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Measure/Complex.lean

deleted theorem MeasureTheory.ComplexMeasure.absolutelyContinuous_eNNReal_iff

added theorem MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

added theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion'

deleted theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adic_completion'

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean