Commit 2023-12-05 14:12 c2164f0f

View on Github →

chore: tidy various files (#8823)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

modified theorem CategoryTheory.ShortComplex.homologyMap_add

modified theorem CategoryTheory.ShortComplex.homologyMap_neg

modified theorem CategoryTheory.ShortComplex.leftHomologyMap_add

modified theorem CategoryTheory.ShortComplex.leftHomologyMap_neg

modified theorem CategoryTheory.ShortComplex.rightHomologyMap_neg

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

added theorem ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable

deleted theorem ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added theorem ContinuousLinearMap.fpowerSeries_apply_one

added theorem ContinuousLinearMap.fpowerSeries_apply_zero

deleted theorem ContinuousLinearMap.fpower_series_apply_one

deleted theorem ContinuousLinearMap.fpower_series_apply_zero

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Nat/Cast/Defs.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Polynomial/FieldDivision.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

Modified Mathlib/Data/Polynomial/UnitTrinomial.lean

Modified Mathlib/Data/Rat/Lemmas.lean

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/Data/Sign.lean

Modified Mathlib/GroupTheory/Subgroup/Finite.lean

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

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

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/RingTheory/Artinian.lean

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

Modified Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean

Modified Mathlib/Topology/GDelta.lean

added theorem isNowhereDense_empty

deleted theorem isNowhereDense_of_empty

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/Support.lean