Commit 2020-08-05 08:29 3b268785

View on Github →

feat(linear_algebra/affine_space): more lemmas (#3615) Add further lemmas on affine spaces. This is the last piece of preparation needed on the affine space side for my definitions of circumcenter and circumradius for a simplex in a Euclidean affine space.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem add_torsor.eq_vadd_iff_vsub_eq

added theorem add_torsor.vsub_set_finite_of_finite

Modified src/linear_algebra/affine_space.lean

added theorem affine_independent_embedding_of_affine_independent

added theorem affine_independent_iff_indicator_eq_of_affine_combination_eq

added theorem affine_independent_subtype_of_affine_independent

added theorem affine_space.finite_dimensional_direction_affine_span_of_finite

added theorem affine_space.finite_dimensional_vector_span_of_finite

added theorem affine_span_disjoint_of_disjoint_of_affine_independent

added theorem affine_subspace.affine_span_coe

added theorem affine_subspace.mem_affine_span_singleton

added theorem exists_mem_inter_of_exists_mem_inter_affine_span_of_affine_independent

added theorem finset.eq_affine_combination_subset_iff_eq_affine_combination_subtype

added theorem finset.eq_weighted_vsub_of_point_subset_iff_eq_weighted_vsub_of_point_subtype

added theorem finset.eq_weighted_vsub_subset_iff_eq_weighted_vsub_subtype

added theorem mem_affine_span_iff_mem_of_affine_independent

added theorem not_mem_affine_span_diff_of_affine_independent