Commit 2023-02-23 12:36 db8c8edf

View on Github →

feat: port LinearAlgebra.LinearIndependent (#2436)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem Fintype.linearIndependent_iff'

added theorem Fintype.linearIndependent_iff

added theorem Fintype.not_linearIndependent_iff

added def LinearIndependent.Maximal

added theorem LinearIndependent.coe_range

added theorem LinearIndependent.comp

added theorem LinearIndependent.disjoint_span_image

added theorem LinearIndependent.eq_of_smul_apply_eq_smul_apply

added theorem LinearIndependent.extend_subset

added theorem LinearIndependent.fin_cons'

added theorem LinearIndependent.fin_cons

added theorem LinearIndependent.group_smul

added theorem LinearIndependent.image

added theorem LinearIndependent.image_of_comp

added theorem LinearIndependent.image_subtype

added theorem LinearIndependent.independent_span_singleton

added theorem LinearIndependent.injective

added theorem LinearIndependent.inl_union_inr

added theorem LinearIndependent.insert

added theorem LinearIndependent.linearIndependent_extend

added theorem LinearIndependent.map'

added theorem LinearIndependent.map

added theorem LinearIndependent.maximal_iff

added theorem LinearIndependent.mono

added theorem LinearIndependent.ne_zero

added theorem LinearIndependent.not_mem_span_image

added theorem LinearIndependent.of_comp

added theorem LinearIndependent.option

added def LinearIndependent.repr

added theorem LinearIndependent.repr_eq

added theorem LinearIndependent.repr_eq_single

added theorem LinearIndependent.repr_ker

added theorem LinearIndependent.repr_range

added theorem LinearIndependent.restrict_of_comp_subtype

added theorem LinearIndependent.restrict_scalars

added theorem LinearIndependent.span_repr_eq

added theorem LinearIndependent.subset_extend

added theorem LinearIndependent.subset_span_extend

added theorem LinearIndependent.sum_type

added theorem LinearIndependent.to_subtype_range'

added theorem LinearIndependent.to_subtype_range

added def LinearIndependent.totalEquiv

added theorem LinearIndependent.totalEquiv_apply_coe

added theorem LinearIndependent.total_comp_repr

added theorem LinearIndependent.total_ne_of_not_mem_support

added theorem LinearIndependent.total_repr

added theorem LinearIndependent.union

added theorem LinearIndependent.units_smul

added def LinearIndependent

added theorem eq_of_linearIndependent_of_span_subtype

added theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span

added theorem exists_linearIndependent

added theorem exists_linearIndependent_extension

added theorem exists_maximal_independent'

added theorem exists_maximal_independent

added theorem exists_of_linearIndependent_of_finite_span

added theorem le_of_span_le_span

added theorem linearDependent_comp_subtype'

added theorem linearDependent_comp_subtype

added theorem linearIndependent_bounded_of_finset_linearIndependent_bounded

added theorem linearIndependent_bunionᵢ_of_directed

added theorem linearIndependent_comp_subtype

added theorem linearIndependent_comp_subtype_disjoint

added theorem linearIndependent_empty

added theorem linearIndependent_empty_type

added theorem linearIndependent_equiv'

added theorem linearIndependent_equiv

added theorem linearIndependent_fin2

added theorem linearIndependent_fin_cons

added theorem linearIndependent_fin_snoc

added theorem linearIndependent_fin_succ'

added theorem linearIndependent_fin_succ

added theorem linearIndependent_finset_map_embedding_subtype

added theorem linearIndependent_iff''

added theorem linearIndependent_iff'

added theorem linearIndependent_iff

added theorem linearIndependent_iff_injective_total

added theorem linearIndependent_iff_not_mem_span

added theorem linearIndependent_iff_not_smul_mem_span

added theorem linearIndependent_iff_totalOn

added theorem linearIndependent_image

added theorem linearIndependent_inl_union_inr'

added theorem linearIndependent_insert'

added theorem linearIndependent_insert

added theorem linearIndependent_monoidHom

added theorem linearIndependent_of_finite

added theorem linearIndependent_of_subsingleton

added theorem linearIndependent_option'

added theorem linearIndependent_option

added theorem linearIndependent_pair

added theorem linearIndependent_singleton

added theorem linearIndependent_span

added theorem linearIndependent_subtype

added theorem linearIndependent_subtype_disjoint

added theorem linearIndependent_subtype_range

added theorem linearIndependent_sum

added theorem linearIndependent_unionᵢ_finite

added theorem linearIndependent_unionᵢ_finite_subtype

added theorem linearIndependent_unionᵢ_of_directed

added theorem linearIndependent_unionₛ_of_directed

added theorem linearIndependent_unique_iff

added theorem mem_span_insert_exchange

added theorem not_linearIndependent_iff

added theorem span_le_span_iff

added theorem surjective_of_linearIndependent_of_span