Prove2Me

`BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero` {A : Module.End ℂ V} {N m : ℕ} (hnil : A ^ N = 0) (hNm : N ≤ m) : A ^ m = 0

Proved
BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylSL2Unipotent.

BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero {A : Module.End ℂ V} {N m : ℕ} (hnil : A ^ N = 0) (hNm : N ≤ m) : A ^ m = 0

Formalization note: Lean 4 identifier BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero.

Preamble
-- Generated from ChapterWeylSL2Unipotent.lean — theorem BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero
import Definitions.Def_ChapterWeylSl2
import Definitions.Def_ChapterWeylSL2Group
import Mathlib
import Definitions.Def_ChapterWeylSL2Unipotent
open BookProof.ChapterWeylSL2Unipotent



open BookProof.ChapterWeylSl2 BookProof.ChapterWeylSL2Group
open Polynomial

universe u

variable {M : Type*} [AddCommGroup M] [Module ℂ M]
variable {V : Type u} [AddCommGroup V] [Module ℂ V]
Formal statement
theorem BookProof.ChapterWeylSL2Unipotent.expSum_pow_eq_zero {A : Module.End ℂ V} {N m : ℕ} (hnil : A ^ N = 0) (hNm : N ≤ m) :
    A ^ m = 0 := by sorry

View graph