Commit 2024-05-27 10:06 85ea1f2b

View on Github →

style: change the notation for CategoryTheory.Limits.piObj from ∏ f to ∏ᶜ f (#13269) This notation is conflicting with ∏ x ∈ s, f x.

Estimated changes

Modified Mathlib/Algebra/Category/FGModuleCat/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Products.lean

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

modified def CommRingCat.piIsoPi

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/CategoryTheory/Adjunction/Evaluation.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Generator.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean

Modified Mathlib/CategoryTheory/Limits/Lattice.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

modified def CategoryTheory.Limits.PreservesProduct.iso

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

modified def CategoryTheory.Limits.biproduct.isoProduct

Modified Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean

modified theorem CategoryTheory.Limits.Concrete.Pi.map_ext

modified theorem CategoryTheory.Limits.Concrete.productEquiv_apply_apply

Modified Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

modified def CategoryTheory.Limits.Multiequalizer.ιPi

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

modified theorem CategoryTheory.Limits.Pi.hom_ext

modified theorem CategoryTheory.Limits.Pi.map'_id_id

modified theorem CategoryTheory.Limits.Pi.map_id

modified def CategoryTheory.Limits.productUniqueIso

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/CategoryTheory/Limits/SmallComplete.lean

Modified Mathlib/CategoryTheory/Preadditive/Injective.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

modified def CategoryTheory.Equalizer.Presieve.Arrows.FirstObj

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

modified def TopCat.piIsoPi

Modified Mathlib/Topology/Sheaves/Sheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean