Commit 2023-05-27 14:37 9f94180e

View on Github →

chore: tidy various files (#4423)

Estimated changes

Modified Mathlib/Algebra/Category/GroupCat/Colimits.lean

Modified Mathlib/Algebra/Category/GroupCat/Images.lean

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

Modified Mathlib/Algebra/Module/Torsion.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean

added theorem AlgebraicGeometry.Polynomial.isOpenMap_comap_C

deleted theorem AlgebraicGeometry.Polynomial.isOpenMap_comap_c

Modified Mathlib/AlgebraicGeometry/SheafedSpace.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

added def BoxIntegral.BoxAdditiveMap.toSMul

added theorem BoxIntegral.BoxAdditiveMap.toSMul_apply

deleted def BoxIntegral.BoxAdditiveMap.toSmul

deleted theorem BoxIntegral.BoxAdditiveMap.toSmul_apply

Modified Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

Modified Mathlib/Combinatorics/Configuration.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/FieldTheory/Separable.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Localization/LocalizationLocalization.lean