Unipotent matrix automorphisms

This file relates unipotence of the natural linear action of an invertible matrix to nilpotence of the matrix obtained by subtracting the identity.

Main declarations

• LinearMap.GeneralLinearGroup.isUnipotent_toLin_iff — a matrix acts unipotently exactly when subtracting the identity from the matrix gives a nilpotent matrix.

theorem LinearMap.GeneralLinearGroup.isUnipotent_toLin_iff (m : Type u_1) [Fintype m] [DecidableEq m] (R : Type u) [CommRing R] (g : GL m R) : (Matrix.GeneralLinearGroup.toLin g).IsUnipotent ↔ IsNilpotent (↑g - 1)

An element of the general linear group is unipotent in its natural representation exactly when subtracting the identity from its underlying matrix gives a nilpotent matrix.