Theorems · Theorem · linear algebra

LinearMap.transvection.baseChange

∀ {R : Type u_3} {V : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_5)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : Module.Dual R V) (v : V),
  LinearMap.baseChange A (LinearMap.transvection f v) =
    LinearMap.transvection ((Module.Dual.baseChange A) f) (1 ⊗ₜ[R] v)

Defined in

Mathlib.LinearAlgebra.Transvection.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAlgebra