Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-20 05:13
dbae2f17
View on Github →
feat: more consistent use of
ext
, and updating porting notes. (
#5242
)
Estimated changes
Modified
Mathlib/Algebra/Category/GroupCat/Basic.lean
Modified
Mathlib/Algebra/Category/GroupCat/Colimits.lean
Modified
Mathlib/Algebra/Category/GroupCat/Limits.lean
Modified
Mathlib/Algebra/Homology/ImageToKernel.lean
Modified
Mathlib/Algebra/Homology/Opposite.lean
Modified
Mathlib/Algebra/Homology/QuasiIso.lean
Modified
Mathlib/AlgebraicGeometry/PresheafedSpace.lean
Modified
Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean
Modified
Mathlib/AlgebraicGeometry/SheafedSpace.lean
added
theorem
AlgebraicGeometry.SheafedSpace.ext
Modified
Mathlib/AlgebraicGeometry/Spec.lean
Modified
Mathlib/AlgebraicGeometry/Stalks.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
deleted
def
SimplicialObject.Splitting.coprod
Modified
Mathlib/CategoryTheory/Abelian/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/Exact.lean
Modified
Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Abelian/Homology.lean
Modified
Mathlib/CategoryTheory/Abelian/Images.lean
Modified
Mathlib/CategoryTheory/Abelian/LeftDerived.lean
Modified
Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
Modified
Mathlib/CategoryTheory/Abelian/Opposite.lean
Modified
Mathlib/CategoryTheory/Abelian/RightDerived.lean
Modified
Mathlib/CategoryTheory/Adjunction/Comma.lean
Modified
Mathlib/CategoryTheory/Closed/Cartesian.lean
Modified
Mathlib/CategoryTheory/Closed/Functor.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/Flat.lean
Modified
Mathlib/CategoryTheory/Idempotents/Basic.lean
Modified
Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
Modified
Mathlib/CategoryTheory/Limits/ConcreteCategory.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/HasLimits.lean
Modified
Mathlib/CategoryTheory/Limits/Over.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Presheaf.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Types.lean
Modified
Mathlib/CategoryTheory/Monad/Products.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mod_.lean
Modified
Mathlib/CategoryTheory/MorphismProperty.lean
Modified
Mathlib/CategoryTheory/Preadditive/Biproducts.lean
Modified
Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
Modified
Mathlib/CategoryTheory/Preadditive/Mat.lean
Modified
Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
Modified
Mathlib/CategoryTheory/Sites/CoverLifting.lean
Modified
Mathlib/CategoryTheory/Sites/Pretopology.lean
Modified
Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
modified
def
CategoryTheory.Equalizer.Presieve.SecondObj
Modified
Mathlib/CategoryTheory/StructuredArrow.lean
Modified
Mathlib/CategoryTheory/Subobject/Lattice.lean
Modified
Mathlib/Topology/Sheaves/Forget.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
Modified
Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
Modified
Mathlib/Topology/Sheaves/Stalks.lean