Commit 2024-12-23 01:07 e8209172

View on Github →

chore: tidy various files (#20184)

Estimated changes

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

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

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

modified theorem AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

modified theorem AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

Modified Mathlib/Analysis/Analytic/OfScalars.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/Calculus/FirstDerivativeTest.lean

Modified Mathlib/CategoryTheory/Comma/Presheaf/Colimit.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

Modified Mathlib/Data/Finset/Max.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Classification.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Modified Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Radical.lean

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/Order/OrderClosedExtr.lean