feat(algebra/char_zero): cast(_pow)_eq_one (#12429)

src/algebra/char_zero.lean

@@ -73,10 +73,20 @@ def cast_embedding : ℕ ↪ R := ⟨coe, cast_injective⟩
 cast_injective.eq_iff
 
 @[simp, norm_cast] theorem cast_eq_zero {n : ℕ} : (n : R) = 0 ↔ n = 0 :=
-by rw [← cast_zero, cast_inj]
+by rw [←cast_zero, cast_inj]
+
+@[simp, norm_cast] theorem cast_eq_one {n : ℕ} : (n : R) = 1 ↔ n = 1 :=
+by rw [←cast_one, cast_inj]
+
+@[simp] lemma cast_pow_eq_one {R : Type*} [semiring R] [char_zero R] (q : ℕ) (n : ℕ) (hn : n ≠ 0) :
+  (q : R) ^ n = 1 ↔ q = 1 :=
+by { rw [←cast_pow, cast_eq_one], exact pow_eq_one_iff hn }
 
 @[norm_cast] theorem cast_ne_zero {n : ℕ} : (n : R) ≠ 0 ↔ n ≠ 0 :=
-not_congr cast_eq_zero
+cast_eq_zero.not
+
+@[norm_cast] theorem cast_ne_one {n : ℕ} : (n : R) ≠ 1 ↔ n ≠ 1 :=
+cast_eq_one.not
 
 lemma cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 :=
 by exact_mod_cast n.succ_ne_zero