Nilpotent maps on finite modules

theorem Module.End.isNilpotent_iff_of_finite {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] {f : End R M} : IsNilpotent f ↔ ∀ (m : M), ∃ (n : ℕ), (f ^ n) m = 0

@[simp]

theorem Matrix.isNilpotent_transpose_iff {R : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq ι] [Fintype ι] {A : Matrix ι ι R} : IsNilpotent A.transpose ↔ IsNilpotent A

theorem Matrix.isNilpotent_iff {R : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq ι] [Fintype ι] {A : Matrix ι ι R} : IsNilpotent A ↔ ∀ (v : ι → R), ∃ (n : ℕ), (A ^ n).mulVec v = 0

theorem Matrix.isNilpotent_iff_forall_row {R : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq ι] [Fintype ι] {A : Matrix ι ι R} : IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).row i = 0

theorem Matrix.isNilpotent_iff_forall_col {R : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq ι] [Fintype ι] {A : Matrix ι ι R} : IsNilpotent A ↔ ∀ (i : ι), ∃ (n : ℕ), (A ^ n).col i = 0