∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v w : V} (hv : f v = 0) (hw : f w = 0)
  (hvw : autoParam (f (v + w) = 0) LinearEquiv.transvection.trans_of_left_eq._auto_1),
  LinearEquiv.transvection hw ≪≫ₗ LinearEquiv.transvection hv = LinearEquiv.transvection hvw