Upper-unitriangular groups in prime characteristic

Let R be a ring of prime characteristic p and m a finite linearly ordered index type. For an upper-unitriangular matrix M, the matrix M - 1 is strictly upper triangular, so its Fintype.card mth power vanishes; since 1 commutes with M - 1, the Frobenius identity then gives M ^ p ^ Fintype.card m = 1. Hence the upper-unitriangular group TauCeti.upperUnitriangularGroup m R is a p-group.

theorem Matrix.IsUpperUnitriangular.pow_eq_one {m : Type u_1} {R : Type u_2} [Fintype m] [LinearOrder m] [Ring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [CharP R p] {M : Matrix m m R} (hM : M.IsUpperUnitriangular) : M ^ p ^ Fintype.card m = 1

An upper-unitriangular m × m matrix over a ring of prime characteristic p has order dividing p ^ Fintype.card m.

theorem TauCeti.isPGroup_upperUnitriangularGroup {m : Type u_1} {R : Type u_2} [Fintype m] [LinearOrder m] [Ring R] {p : ℕ} [Fact (Nat.Prime p)] [CharP R p] : IsPGroup p ↥(upperUnitriangularGroup m R)

Over a ring of prime characteristic p, the upper-unitriangular group is a p-group.