isNilpotent_transpose_iff — Mathlib

English

For a square matrix A over a commutative semiring, A^T is nilpotent if and only if A is nilpotent.

Русский

Для квадратной матрицы A над коммутативным полем, A^T нильпотентна тогда и только тогда, когда A нильпотентна.

LaTeX

$$$\\operatorname{IsNilpotent}(A^{T}) \\iff \\operatorname{IsNilpotent}(A).$$$

Lean4

@[simp]
theorem isNilpotent_transpose_iff : IsNilpotent Aᵀ ↔ IsNilpotent A := by
  simp_rw [IsNilpotent, ← transpose_pow, transpose_eq_zero]

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