English
In a ring with ringChar ≠ 2, the integers embed injectively on {0,1,-1}.
Русский
В кольце с ringChar ≠ 2 целые числа внедряются инъективно на {0,1,-1}.
LaTeX
$$$ {R} [NonAssocRing R] [Nontrivial R] (hR : ringChar R \neq 2) : ({0,1,-1} : Set \mathbb{Z}).InjOn (Int.cast : \mathbb{Z} \to R) $$$
Lean4
/-- If two integers from `{0, 1, -1}` result in equal elements in a ring `R`
that is nontrivial and of characteristic not `2`, then they are equal. -/
theorem cast_injOn_of_ringChar_ne_two {R : Type*} [NonAssocRing R] [Nontrivial R] (hR : ringChar R ≠ 2) :
({0, 1, -1} : Set ℤ).InjOn ((↑) : ℤ → R) :=
by
rintro _ (rfl | rfl | rfl) _ (rfl | rfl | rfl) h <;>
simp only [cast_neg, cast_one, cast_zero, neg_eq_zero, one_ne_zero, zero_ne_one, zero_eq_neg] at h ⊢
· exact ((Ring.neg_one_ne_one_of_char_ne_two hR).symm h).elim
· exact ((Ring.neg_one_ne_one_of_char_ne_two hR) h).elim
