α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q (↑(monomial E.order) 1 - ∑ i : Fin E.order, ↑(monomial ↑i) (coeffs E i)) = 0
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ IsRoot (charPoly E) q
rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔
    eval₂ (RingHom.id α) q (↑(monomial E.order) 1 - ∑ i : Fin E.order, ↑(monomial ↑i) (coeffs E i)) = 0
simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
  Polynomial.eval₂_sub]
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0

case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0 → IsSolution E fun n => q ^ n
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
constructor
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : IsSolution E fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ (IsSolution E fun n => q ^ n) → q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
intro h
no goals
case mp
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : IsSolution E fun n => q ^ n
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
simpa [sub_eq_zero] using h 0
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (fun n => q ^ n) (n + ↑i)
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
⊢ q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0 → IsSolution E fun n => q ^ n
intro h n
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ ∑ x : Fin E.order, q ^ n * (coeffs E x * q ^ ↑x) = ∑ x : Fin E.order, coeffs E x * (q ^ n * q ^ ↑x)
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ (fun n => q ^ n) (n + E.order) = ∑ i : Fin E.order, coeffs E i * (fun n => q ^ n) (n + ↑i)
simp only [pow_add, sub_eq_zero.mp h, mul_sum]
no goals
case mpr
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
⊢ ∑ x : Fin E.order, q ^ n * (coeffs E x * q ^ ↑x) = ∑ x : Fin E.order, coeffs E x * (q ^ n * q ^ ↑x)
exact sum_congr rfl fun _ _ ↦ by ring
no goals
α : Type u_1
inst✝ : CommRing α
E : LinearRecurrence α
q : α
h : q ^ E.order - ∑ x : Fin E.order, coeffs E x * q ^ ↑x = 0
n : ℕ
x✝¹ : Fin E.order
x✝ : x✝¹ ∈ univ
⊢ q ^ n * (coeffs E x✝¹ * q ^ ↑x✝¹) = coeffs E x✝¹ * (q ^ n * q ^ ↑x✝¹)
ring