Commit 2021-04-07 10:30 df8ef379

View on Github →

feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058) Besides the title lemma, this PR also moves lemma is_unit_int from algebra/associated to data/int/basic.

Estimated changes

Modified src/algebra/associated.lean

deleted theorem is_unit_int

Modified src/algebra/ring/basic.lean

added theorem is_unit.neg

Modified src/data/int/basic.lean

added theorem int.is_unit_eq_one_or

added theorem int.is_unit_iff

added theorem int.is_unit_iff_nat_abs_eq

added theorem int.nat_abs_eq_iff

Modified src/ring_theory/int/basic.lean