eq_zero_of_isNilpotent_isSemisimple

English

If an endomorphism f is nilpotent and semisimple, then f must be the zero map.

Русский

Если концевое отображение f нильпотентно и полносемпсимально, то оно равно нулю.

LaTeX

$$$ IsNilpotent(f) \land IsSemisimple(f) \Rightarrow f = 0$$$

Lean4

theorem eq_zero_of_isNilpotent_isSemisimple (hn : IsNilpotent f) (hs : f.IsSemisimple) : f = 0 :=
  by
  have ⟨n, h0⟩ := hn
  rw [← aeval_X (R := R) f]; rw [← aeval_X_pow (R := R) f] at h0
  rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢
  exact hs.annihilator_isRadical _ _ ⟨n, h0⟩

Похожие утверждения