Theorems · Theorem · group theory

Matrix.SpecialLinearGroup.transvection_smul_single_snd

∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  Matrix.SpecialLinearGroup.transvection hij b • Pi.single j 1 = Pi.single j 1 + b • Pi.single i 1

The transvection transvection i j hij b acts on e_j = Pi.single j 1 by adding b·e_i.

Defined in

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommRing