Commit 2024-04-04 10:53 3e060f08

View on Github →

chore: Remove Init.Data.Int.CompLemmas (#11882) Most lemmas are too specific to be reused so I deleted them. They must have been used for tactics in Lean 3. I moved the few lemmas that were generally useful (although I could only see one use, in RingTheory.Localization.Away.Basic!) to Data.Int.Defs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Int/Defs.lean

added theorem Int.natAbs_add_of_nonneg

added theorem Int.natAbs_add_of_nonpos

added theorem Int.natAbs_ofNat'

added theorem Int.zero_le_ofNat

Deleted Mathlib/Init/Data/Int/CompLemmas.lean

deleted theorem Int.natAbs_ofNat_core

deleted theorem Int.natAbs_of_negSucc

deleted theorem Int.ne_of_natAbs_ne_natAbs_of_nonneg

deleted theorem Int.zero_le_ofNat

Modified Mathlib/RingTheory/Localization/Away/Basic.lean