Commit 2020-09-18 08:44 b00b01f2

View on Github →

feat(linear_algebra/affine_space): more lemmas (#4127) Add another batch of lemmas relating to affine spaces. These include factoring out vector_span_mono as a combination of two other lemmas that's used several times, and additional variants of lemmas relating to finite-dimensional subspaces.

Estimated changes

Modified src/linear_algebra/affine_space/basic.lean

added theorem affine_subspace.eq_iff_direction_eq_of_mem

added theorem affine_subspace.eq_of_direction_eq_of_nonempty_of_le

added theorem vector_span_mono

Modified src/linear_algebra/affine_space/finite_dimensional.lean

added theorem affine_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one

added theorem affine_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one

added theorem findim_vector_span_image_finset_of_affine_independent

added theorem vector_span_eq_of_le_of_affine_independent_of_card_eq_findim_add_one

added theorem vector_span_image_finset_eq_of_le_of_affine_independent_of_card_eq_findim_add_one