UnipotentGroupNilpotent.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Nilpotence from a faithful upper-unipotent representation

The entry filtration records the diagonal on which a matrix can first be nonzero. Commutators advance this filtration. The finite matrix size then bounds the lower central series of the represented group.

def OAI.PolycyclicRecognition.MatrixDepth line 21
Source documentation
Vanishing on all diagonals strictly below the k-th upper diagonal.
```
def MatrixDepth (k : ℕ) (X : Matrix (Fin n) (Fin n) R) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.MatrixDepth.zero line 26
theorem OAI.PolycyclicRecognition.MatrixDepth.mono line 30
theorem OAI.PolycyclicRecognition.MatrixDepth.add line 35
theorem OAI.PolycyclicRecognition.MatrixDepth.neg line 40
theorem OAI.PolycyclicRecognition.MatrixDepth.sub line 45
theorem OAI.PolycyclicRecognition.MatrixDepth.mul line 49
theorem OAI.PolycyclicRecognition.MatrixDepth.one line 60
theorem OAI.PolycyclicRecognition.MatrixDepth.eq_zero line 65
theorem OAI.PolycyclicRecognition.MatrixDepth.of_strictUpper line 70
theorem OAI.PolycyclicRecognition.nilpotent_of_faithful_strictUpper_representation line 81
Source documentation
A common finite upper-unipotent realization bounds the group lower central series, without any finiteness assumption on the represented group.
```
theorem nilpotent_of_faithful_strictUpper_representation
    (ρ : H →* (Matrix (Fin n) (Fin n) R)ˣ) (hinj : Function.Injective ρ)
    (hu : ∀ h, StrictUpper ((ρ h : Matrix (Fin n) (Fin n) R) - 1)) :
    Group.IsNilpotent H := by
…
```
Mentions: OAI.PolycyclicRecognition.StrictUpper