def Matrix.GeneralLinearGroup.diagonalHom (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] : (n → Rˣ) →* GL n R

The multiplicative group homomorphism (Rˣ)ⁿ →* GL(n, R) given by mapping a vector x to Matrix.diagonal x.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.GeneralLinearGroup.diagonalSubgroup (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] : Subgroup (GL n R)

The group of invertible diagonal matrices.

Equations

• Matrix.GeneralLinearGroup.diagonalSubgroup n R = Subgroup.map (Matrix.GeneralLinearGroup.diagonalHom n R) ⊤