∀ {k : Type u_3} {P₁ : Type u_1} {V₁ : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (u : (P₁ →ᵃ[k] P₁)ˣ) (x : P₁) (x_1 : V₁), ↑u (x_1 +ᵥ x) = (↑u).linear x_1 +ᵥ ↑u x