Skip to content

Commit fa813a8

Browse files
committed
feat(Int/Units): a few lemmas about ℤˣ (#6933)
1 parent 57559c5 commit fa813a8

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

Mathlib/Data/Int/Units.lean

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,18 @@ theorem units_eq_one_or (u : ℤˣ) : u = 1 ∨ u = -1 := by
3030
simpa only [Units.ext_iff, units_natAbs] using natAbs_eq u
3131
#align int.units_eq_one_or Int.units_eq_one_or
3232

33+
@[simp]
34+
theorem units_ne_neg_self (u : ℤˣ) : u ≠ -u := by
35+
rcases units_eq_one_or u with rfl | rfl <;> decide
36+
37+
@[simp]
38+
theorem neg_units_ne_self (u : ℤˣ) : -u ≠ u := (units_ne_neg_self u).symm
39+
40+
theorem units_ne_iff_eq_neg {u u' : ℤˣ} : u ≠ u' ↔ u = -u' := by
41+
rcases units_eq_one_or u with rfl | rfl <;>
42+
rcases units_eq_one_or u' with rfl | rfl <;>
43+
decide
44+
3345
theorem isUnit_eq_one_or {a : ℤ} : IsUnit a → a = 1 ∨ a = -1
3446
| ⟨_, hx⟩ => hx ▸ (units_eq_one_or _).imp (congr_arg Units.val) (congr_arg Units.val)
3547
#align int.is_unit_eq_one_or Int.isUnit_eq_one_or

0 commit comments

Comments
 (0)