Theorems · Theorem · linear algebra

LinearEquiv.transvection.trans_of_right_eq

∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f g : Module.Dual R V}
  {v : V} (hf : f v = 0) (hg : g v = 0)
  (hfg : autoParam ((f + g) v = 0) LinearEquiv.transvection.trans_of_right_eq._auto_1),
  LinearEquiv.transvection hg ≪≫ₗ LinearEquiv.transvection hf = LinearEquiv.transvection hfg

Defined in

Mathlib.LinearAlgebra.Transvection.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModule