Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-22 06:38 03f0285d

View on Github →

refactor(algebra/add_torsor): define pointwise -ᵥ and +ᵥ on sets (#4710) This seems more natural than vsub_set to me.

Estimated changes

added theorem set.empty_vsub
added theorem set.finite.vadd
added theorem set.finite.vsub
added theorem set.singleton_vadd
added theorem set.singleton_vsub
added theorem set.vadd_singleton
added theorem set.vadd_subset_vadd
added theorem set.vsub_empty
added theorem set.vsub_mem_vsub
added theorem set.vsub_self_mono
added theorem set.vsub_singleton
added theorem set.vsub_subset_iff
added theorem set.vsub_subset_vsub
deleted theorem vsub_mem_vsub_set
deleted def vsub_set
deleted theorem vsub_set_empty
deleted theorem vsub_set_finite_of_finite
deleted theorem vsub_set_mono
deleted theorem vsub_set_singleton
modified def vector_span
modified theorem vector_span_def
modified theorem vsub_set_subset_vector_span