Commit 2024-04-04 22:42 483848e8

View on Github →

chore: tidy various files (#11624)

Estimated changes

Modified Archive/Wiedijk100Theorems/CubingACube.lean

Modified Mathlib/Algebra/Divisibility/Units.lean

modified theorem IsRelPrime.mul_right

Modified Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

Modified Mathlib/Algebra/Order/Monoid/MinMax.lean

Modified Mathlib/Algebra/Ring/InjSurj.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

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

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

Modified Mathlib/Data/Polynomial/Eval.lean

Modified Mathlib/Data/Real/EReal.lean

Modified Mathlib/Data/Set/Lattice.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

modified theorem SmoothPartitionOfUnity.eventually_fintsupport_subset

modified def SmoothPartitionOfUnity.fintsupport

Modified Mathlib/GroupTheory/Perm/Cycle/Factors.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

modified theorem Function.FactorsThrough.comp_left

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean

modified theorem BoundedContinuousFunction.integrable_of_nnreal

modified theorem BoundedContinuousFunction.lintegral_lt_top_of_nnreal

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Modified Mathlib/MeasureTheory/Measure/Count.lean

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/NumberTheory/SmoothNumbers.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/RingTheory/AlgebraTower.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/Coprime/Lemmas.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

modified theorem PowerSeries.order_eq_top

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean