Commit 2023-12-20 10:04 95ddd894

View on Github →

chore: tidy various files (#9016)

Estimated changes

Modified Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/FieldTheory/RatFunc.lean

Modified Mathlib/Logic/Equiv/Defs.lean

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

modified theorem isPiSystem_isClosed

modified theorem isPiSystem_isOpen

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

Modified Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

added theorem MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure

added theorem MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/Testing/SlimCheck/Functions.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean