Commit 2023-04-21 08:03 94d947db

View on Github →

feat: port LinearAlgebra.AffineSpace.Independent (#3341)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Independent.lean

added theorem Affine.Simplex.centroid_eq_iff

added theorem Affine.Simplex.centroid_eq_of_range_eq

added theorem Affine.Simplex.ext

added theorem Affine.Simplex.ext_iff

added def Affine.Simplex.face

added theorem Affine.Simplex.face_centroid_eq_centroid

added theorem Affine.Simplex.face_centroid_eq_iff

added theorem Affine.Simplex.face_eq_mkOfPoint

added theorem Affine.Simplex.face_points'

added theorem Affine.Simplex.face_points

added def Affine.Simplex.mkOfPoint

added theorem Affine.Simplex.mkOfPoint_points

added theorem Affine.Simplex.range_face_points

added def Affine.Simplex.reindex

added theorem Affine.Simplex.reindex_range_points

added theorem Affine.Simplex.reindex_refl

added theorem Affine.Simplex.reindex_reindex_symm

added theorem Affine.Simplex.reindex_symm_reindex

added theorem Affine.Simplex.reindex_trans

added structure Affine.Simplex

added theorem AffineEquiv.affineIndependent_iff

added theorem AffineEquiv.affineIndependent_set_of_eq_iff

added theorem AffineIndependent.affineIndependent_of_not_mem_span

added theorem AffineIndependent.affineSpan_disjoint_of_disjoint

added theorem AffineIndependent.comp_embedding

added theorem AffineIndependent.exists_mem_inter_of_exists_mem_inter_affineSpan

added theorem AffineIndependent.indicator_eq_of_affineCombination_eq

added theorem AffineIndependent.map'

added theorem AffineIndependent.not_mem_affineSpan_diff

added theorem AffineIndependent.of_comp

added theorem AffineIndependent.of_set_of_injective

added theorem AffineIndependent.units_lineMap

added def AffineIndependent

added theorem AffineMap.affineIndependent_iff

added theorem affineCombination_mem_affineSpan_pair

added theorem affineIndependent_def

added theorem affineIndependent_equiv

added theorem affineIndependent_iff

added theorem affineIndependent_iff_eq_of_fintype_affineCombination_eq

added theorem affineIndependent_iff_indicator_eq_of_affineCombination_eq

added theorem affineIndependent_iff_linearIndependent_vsub

added theorem affineIndependent_iff_of_fintype

added theorem affineIndependent_of_ne

added theorem affineIndependent_of_ne_of_mem_of_mem_of_not_mem

added theorem affineIndependent_of_ne_of_mem_of_not_mem_of_mem

added theorem affineIndependent_of_ne_of_not_mem_of_mem_of_mem

added theorem affineIndependent_of_subsingleton

added theorem affineIndependent_set_iff_linearIndependent_vsub

added theorem exists_affineIndependent

added theorem exists_nontrivial_relation_sum_zero_of_not_affine_ind

added theorem exists_subset_affineIndependent_affineSpan_eq_top

added theorem linearIndependent_set_iff_affineIndependent_vadd_union_singleton

added theorem sign_eq_of_affineCombination_mem_affineSpan_pair

added theorem sign_eq_of_affineCombination_mem_affineSpan_single_lineMap

added theorem weightedVSub_mem_vectorSpan_pair