Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 17:25 c32d01d7

View on Github →

feat(algebra/linear_algebra): add basic theory on linear algebra

Estimated changes

Created algebra/linear_algebra/basic.lean

added theorem constr_add

added theorem constr_basis

added theorem constr_congr

added theorem constr_eq

added theorem constr_im_eq_span

added theorem constr_mem_span

added theorem constr_neg

added theorem constr_smul

added theorem constr_sub

added theorem constr_zero

added theorem eq_of_linear_independent_of_span

added theorem exists_finite_card_le_of_finite_of_linear_independent_of_span

added theorem exists_is_basis

added theorem exists_left_inverse_linear_map_of_injective

added theorem exists_linear_independent

added theorem exists_of_linear_independent_of_finite_span

added theorem exists_right_inverse_linear_map_of_surjective

added theorem finset.smul_sum

added theorem finsupp.smul_sum

added def is_basis.constr

added theorem is_basis.eq_linear_map

added theorem is_basis.map_constr

added theorem is_basis.map_repr

added def is_basis

added theorem is_linear_map.finsupp_sum

added theorem is_submodule_range_smul

added theorem is_submodule_span

added theorem lc.is_linear_map_sum

added theorem lc.smul_apply

added theorem lc.sum_smul_index

added def lc

added theorem linear_eq_on

added theorem linear_independent.eq_0_of_span

added theorem linear_independent.image

added theorem linear_independent.inj_span_iff_inj

added theorem linear_independent.insert

added theorem linear_independent.mono

added theorem linear_independent.of_image

added def linear_independent.repr

added theorem linear_independent.unique

added def linear_independent

added theorem linear_independent_Union_of_directed

added theorem linear_independent_bUnion_of_directed

added theorem linear_independent_empty

added theorem linear_independent_iff_not_mem_span

added theorem linear_map.linear_independent_image_iff

added theorem mem_span_insert_exchange

added def module_equiv_lc

added theorem repr_add

added theorem repr_eq

added theorem repr_eq_repr_of_subset

added theorem repr_eq_single

added theorem repr_eq_zero

added theorem repr_finsupp_sum

added theorem repr_neg

added theorem repr_not_span

added theorem repr_smul

added theorem repr_spec

added theorem repr_sub

added theorem repr_sum

added theorem repr_sum_eq

added theorem repr_support

added theorem repr_zero

added def span

added theorem span_empty

added theorem span_eq

added theorem span_eq_of_is_submodule

added theorem span_image_of_linear_map

added theorem span_insert

added theorem span_insert_eq_span

added theorem span_minimal

added theorem span_mono

added theorem span_singleton

added theorem span_span

added theorem span_union

added theorem subset_span

added theorem zero_not_mem_of_linear_independent

Created algebra/linear_algebra/default.lean