Commit 2025-01-10 00:02 e44f03d6

View on Github →

chore: remove more erws (#20605)

Estimated changes

Modified Mathlib/Algebra/Category/Grp/AB.lean

Modified Mathlib/Algebra/Order/Antidiag/Prod.lean

Modified Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

Modified Mathlib/Algebra/Order/Monovary.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added theorem CategoryTheory.Limits.colimMap_eq

added theorem CategoryTheory.Limits.limMap_eq

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

Modified Mathlib/Data/Finset/Prod.lean

added theorem Finset.product_eq_sprod

Modified Mathlib/Order/BooleanAlgebra.lean

Modified Mathlib/Order/Filter/Bases.lean

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Order/RelSeries.lean