Theorems · Theorem · linear algebra

LinearEquiv.dilatransvection.baseChange

∀ {R : Type u_3} {V : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : CommRing A] [inst_4 : Algebra R A],
  ∀ e ∈ LinearEquiv.dilatransvections R V,
    LinearEquiv.baseChange R A V V e ∈ LinearEquiv.dilatransvections A (TensorProduct R A V)

Defined in

Mathlib.LinearAlgebra.Transvection.Basic

Cited by

0 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Quot.sound

Assumes

CommRingAddCommGroupModuleCommRingAlgebra