R : Type u
S : Type ?u.665456
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), ↑(Finsupp.total ℕ ((fun x => M) v) R fun n => ↑(f ^ n) v) l = 0 → l = 0) ↔
    ∀ (p : R[X]), ↑(↑(aeval f) p) v = 0 → p = 0
R : Type u
S : Type ?u.665456
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (LinearIndependent R fun n => ↑(f ^ n) v) ↔ ∀ (p : R[X]), ↑(↑(aeval f) p) v = 0 → p = 0
rw [linearIndependent_iff]
R : Type u
S : Type ?u.665456
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (Finsupp.sum l fun i a => a • ↑(f ^ i) v) = 0 → l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ), (sum { toFinsupp := q } fun n b => b • ↑(f ^ n) v) = 0 → q = 0
R : Type u
S : Type ?u.665456
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), ↑(Finsupp.total ℕ ((fun x => M) v) R fun n => ↑(f ^ n) v) l = 0 → l = 0) ↔
    ∀ (p : R[X]), ↑(↑(aeval f) p) v = 0 → p = 0
simp only [Finsupp.total_apply, aeval_endomorphism, forall_iff_forall_finsupp, Sum, support,
  coeff, ofFinsupp_eq_zero]
no goals
R : Type u
S : Type ?u.665456
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (Finsupp.sum l fun i a => a • ↑(f ^ i) v) = 0 → l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ), (sum { toFinsupp := q } fun n b => b • ↑(f ^ n) v) = 0 → q = 0
exact Iff.rfl