Commit 2024-02-09 22:56 1c8a8a8e

View on Github →

chore: tidy various files (#10362)

Estimated changes

Modified Archive/Hairer.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

Modified Mathlib/Analysis/Complex/Basic.lean

modified theorem Complex.mem_slitPlane_iff

modified theorem Complex.slitPlane_eq_union

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/Pretopology.lean

Modified Mathlib/CategoryTheory/Sites/Spaces.lean

modified def Opens.grothendieckTopology

modified def Opens.pretopology

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Data/Complex/Order.lean

added theorem Complex.nonneg_iff

added theorem Complex.pos_iff

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Nat/Factorial/SuperFactorial.lean

modified theorem Nat.prod_range_factorial_succ

Modified Mathlib/Dynamics/Ergodic/Conservative.lean

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

modified theorem IsIntegralCurve.continuous

Modified Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean

modified def IsFreeGroup.basis

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

Modified Mathlib/MeasureTheory/Constructions/Projective.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/SetSemiring.lean

Modified Mathlib/Order/Filter/NAry.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/RingTheory/Nilpotent.lean

Modified Mathlib/RingTheory/Perfection.lean

Modified Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean

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

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean