Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.nat_abs_eq_iff

Modification history

2021-04-07 10:30

src/data/int/basic.lean

feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058) …

Added int.nat_abs_eq_iff View on Github →