Commit 2024-03-26 06:36 01a0b4e6

View on Github →

chore(Init/Data/Int): drop deprecated lemmas (#11664) Cherry-picked from #9607

Estimated changes

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

deleted theorem Int.eq_zero_of_natAbs_eq_zero

deleted theorem Int.natAbs_pos_of_ne_zero