Commit 2023-05-03 13:39 b44bbff1

View on Github →

feat: port LinearAlgebra.AffineSpace.FiniteDimensional (#3670)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean

added theorem Affine.Simplex.span_eq_top

added theorem AffineBasis.card_eq_finrank_add_one

added theorem AffineBasis.exists_affineBasis_of_finiteDimensional

added theorem AffineIndependent.affineSpan_eq_of_le_of_card_eq_finrank_add_one

added theorem AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one

added theorem AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one

added theorem AffineIndependent.finrank_vectorSpan

added theorem AffineIndependent.finrank_vectorSpan_image_finset

added theorem AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one

added theorem AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one

added theorem AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one

added theorem Collinear.affineSpan_eq_of_ne

added theorem Collinear.collinear_insert_iff_of_ne

added theorem Collinear.coplanar

added theorem Collinear.coplanar_insert

added theorem Collinear.finiteDimensional_direction_affineSpan

added theorem Collinear.finiteDimensional_vectorSpan

added theorem Collinear.mem_affineSpan_of_mem_of_ne

added theorem Collinear.subset

added def Collinear

added theorem Coplanar.finiteDimensional_direction_affineSpan

added theorem Coplanar.finiteDimensional_vectorSpan

added theorem Coplanar.subset

added def Coplanar

added theorem affineIndependent_iff_finrank_vectorSpan_eq

added theorem affineIndependent_iff_le_finrank_vectorSpan

added theorem affineIndependent_iff_not_collinear

added theorem affineIndependent_iff_not_collinear_of_ne

added theorem affineIndependent_iff_not_collinear_set

added theorem affineIndependent_iff_not_finrank_vectorSpan_le

added theorem collinear_empty

added theorem collinear_iff_exists_forall_eq_smul_vadd

added theorem collinear_iff_finrank_le_one

added theorem collinear_iff_not_affineIndependent

added theorem collinear_iff_not_affineIndependent_of_ne

added theorem collinear_iff_not_affineIndependent_set

added theorem collinear_iff_of_mem

added theorem collinear_iff_rank_le_one

added theorem collinear_insert_iff_of_mem_affineSpan

added theorem collinear_insert_insert_insert_left_of_mem_affineSpan_pair

added theorem collinear_insert_insert_insert_of_mem_affineSpan_pair

added theorem collinear_insert_insert_of_mem_affineSpan_pair

added theorem collinear_insert_of_mem_affineSpan_pair

added theorem collinear_pair

added theorem collinear_singleton

added theorem collinear_triple_of_mem_affineSpan_pair

added theorem coplanar_empty

added theorem coplanar_iff_finrank_le_two

added theorem coplanar_insert_iff_of_mem_affineSpan

added theorem coplanar_of_fact_finrank_eq_two

added theorem coplanar_of_finrank_eq_two

added theorem coplanar_pair

added theorem coplanar_singleton

added theorem coplanar_triple

added theorem finiteDimensional_direction_affineSpan_of_finite

added theorem finiteDimensional_vectorSpan_of_finite

added theorem finite_of_fin_dim_affineIndependent

added theorem finite_set_of_fin_dim_affineIndependent

added theorem finrank_vectorSpan_image_finset_le

added theorem finrank_vectorSpan_insert_le

added theorem finrank_vectorSpan_insert_le_set

added theorem finrank_vectorSpan_le_iff_not_affineIndependent

added theorem finrank_vectorSpan_range_le

added theorem ne₁₂_of_not_collinear

added theorem ne₁₃_of_not_collinear

added theorem ne₂₃_of_not_collinear