Commit 2023-06-20 11:14 eb948e46

View on Github →

feat: port Mathlib.Init.Data.Int.CompLemmas (#5269)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Init/Data/Int/Basic.lean

deleted theorem Int.natAbs_add_neg

deleted theorem Int.natAbs_add_nonneg

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

added theorem Int.natAbs_ofNat_core

added theorem Int.natAbs_of_negSucc

added theorem Int.ne_of_natAbs_ne_natAbs_of_nonneg

added theorem Int.zero_le_ofNat

Modified Mathlib/Init/Data/Int/Order.lean

Modified Mathlib/NumberTheory/LegendreSymbol/Basic.lean

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