R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) 2 = 2
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0
suffices eval (x + y) 2 = 2 by convert this <;> norm_num
no goals
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) 2 = 2
exact eval_nat_cast
no goals
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
this : eval (x + y) 2 = 2
⊢ eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0
convert this <;> norm_num
no goals
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 1) = x ^ 1 + y ^ 1
simp only [eval_X, dickson_one, pow_one]
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two,
  C_1, eval_one]
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
conv_lhs => simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
no goals
R : Type u_1
S : Type ?u.117133
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
ring