Commit 2024-01-12 12:47 f34cd078

View on Github →

perf (CategoryTheory.ComposableArrows): swap out linarith for omega (#9594) This file now has the lead in the number of CPU instructions amongst all of mathlib. The majority come from linarith being an autoparam for many definitions, often in multiple arguments. This uses omega in place of linarith to improve performance.

Estimated changes

Modified Mathlib/Algebra/Homology/ExactSequence.lean

modified theorem CategoryTheory.ComposableArrows.Exact.exact'

modified theorem CategoryTheory.ComposableArrows.IsComplex.zero'

modified def CategoryTheory.ComposableArrows.sc'

Modified Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

Modified Mathlib/CategoryTheory/ComposableArrows.lean

modified def CategoryTheory.ComposableArrows.arrow

modified theorem CategoryTheory.ComposableArrows.homMk₂_app_two

modified theorem CategoryTheory.ComposableArrows.homMk₃_app_three

modified theorem CategoryTheory.ComposableArrows.homMk₃_app_two

modified theorem CategoryTheory.ComposableArrows.map'_comp

added theorem CategoryTheory.ComposableArrows.map'_inv_eq_inv_map'

modified theorem CategoryTheory.ComposableArrows.map'_self

modified theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_arrow

modified theorem CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_map_succ

modified theorem CategoryTheory.ComposableArrows.naturality'