Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 12:54 593b1bb5

View on Github →

feat(linear_algebra/affine_space): lemmas on affine spans (#3453) Add more lemmas on affine spans; in particular, that the points in an affine_span are exactly the affine_combinations where the sum of weights equals 1, provided the underlying ring is nontrivial.

Estimated changes

Modified src/linear_algebra/affine_space.lean

added theorem affine_space.affine_combination_mem_affine_span

added theorem affine_space.affine_span_nonempty

added theorem affine_space.eq_affine_combination_of_mem_affine_span

added theorem affine_space.mem_affine_span_iff_eq_affine_combination

added theorem affine_space.mem_vector_span_iff_eq_weighted_vsub

added theorem affine_space.span_points_nonempty

deleted theorem affine_space.span_points_nonempty_of_nonempty

added theorem affine_space.vector_span_empty

added theorem affine_space.vector_span_eq_span_vsub_set_left

added theorem affine_space.vector_span_eq_span_vsub_set_right

added theorem affine_space.vector_span_range_eq_span_range_vsub_left

added theorem affine_space.vector_span_range_eq_span_range_vsub_right

added theorem affine_space.weighted_vsub_mem_vector_span

added theorem finset.affine_combination_apply

added theorem finset.affine_combination_indicator_subset

added theorem finset.affine_combination_of_eq_one_of_eq_zero

added theorem finset.weighted_vsub_empty

added theorem finset.weighted_vsub_indicator_subset

added theorem finset.weighted_vsub_of_point_indicator_subset