∀ {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 : V} (hfv : f v = 0), LinearEquiv.transvection hfv ∈ LinearEquiv.transvections R V