Documentation

PFR.Mathlib.Algebra.AddTorsor

@[simp]
theorem Set.vadd_set_vsub_vadd_set {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] (v : G) (s t : Set P) :
v +ᵥ s -ᵥ (v +ᵥ t) = s -ᵥ t