Theorems · Theorem · group theory

Matrix.GeneralLinearGroup.upperRightHom_apply

∀ {R : Type u_1} [inst : Ring R] (x : R),
  Matrix.GeneralLinearGroup.upperRightHom x =
    { val := !![1, x; 0, 1], inv := !![1, -x; 0, 1], val_inv := ⋯, inv_val := ⋯ }

Defined in

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Cited by

8 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring