isNilpotent_trace_of_isNilpotent — Mathlib

English

If a linear map f is nilpotent, then its trace is nilpotent as an element of R.

Русский

Если линейное отображение f нильпотентно, то его след является нильпотентом в кольце R.

LaTeX

$$$ \text{IsNilpotent}(f) \Rightarrow \operatorname{IsNilpotent}(\operatorname{trace}_R M f). $$$

Lean4

theorem isNilpotent_trace_of_isNilpotent {f : M →ₗ[R] M} (hf : IsNilpotent f) : IsNilpotent (trace R M f) :=
  by
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  swap
  · rw [LinearMap.trace, dif_neg H]
    exact IsNilpotent.zero
  obtain ⟨s, ⟨b⟩⟩ := H
  classical
  rw [trace_eq_matrix_trace R b]
  apply Matrix.isNilpotent_trace_of_isNilpotent
  simpa

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