def Matrix.GeneralLinearGroup.diagonal {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (d : n → Rˣ) : GL n R

The invertible diagonal matrix associated to a vector of units (the diagonal entries).

noncomputable def Matrix.GeneralLinearGroup.GL2.unipotent {R : Type u_2} [CommRing R] (t : R) : GL (Fin 2) R

The unipotent matrix element !![1, t; 0, 1].

theorem Matrix.GeneralLinearGroup.GL2.unipotent_def {R : Type u_2} [CommRing R] (t : R) : ↑(unipotent t) = !![1, t; 0, 1]

theorem Matrix.GeneralLinearGroup.GL2.unipotent_inv {R : Type u_2} [CommRing R] (t : R) : (unipotent t)⁻¹ = unipotent (-t)

theorem Matrix.GeneralLinearGroup.GL2.unipotent_mul {R : Type u_2} [CommRing R] (t₁ t₂ : R) : unipotent t₂ * unipotent t₁ = unipotent (t₁ + t₂)