Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-05 09:21 682f4b5a

View on Github →

feat(linear_algebra): module (vector space) structure for finsupp, matrix, and mv polynomials

Estimated changes

Modified src/data/finsupp.lean

added def finsupp.equiv_fun_on_fintype

added theorem finsupp.ext_iff

added theorem finsupp.filter_curry

added theorem finsupp.filter_sum

added theorem finsupp.filter_zero

added theorem finsupp.injective_single

added theorem finsupp.map_domain_apply

added theorem finsupp.map_domain_notin_range

added theorem finsupp.map_range_finset_sum

added theorem finsupp.map_range_multiset_sum

added def finsupp.restrict_support_equiv

added theorem finsupp.single_eq_single_iff

added theorem finsupp.support_curry

Modified src/data/multivariate_polynomial.lean

added theorem mv_polynomial.smul_eq_C_mul

added theorem mv_polynomial.smul_eval

Modified src/field_theory/finite.lean

modified def finite_field.field_of_integral_domain

added theorem finite_field.pow_card_sub_one_eq_one

Created src/field_theory/mv_polynomial.lean

added def mv_polynomial.R

added theorem mv_polynomial.degrees_indicator

added theorem mv_polynomial.dim_R

added theorem mv_polynomial.eq_zero_of_eval_eq_zero

added theorem mv_polynomial.eval_indicator_apply_eq_one

added theorem mv_polynomial.eval_indicator_apply_eq_zero

added def mv_polynomial.evalᵢ

added def mv_polynomial.evalₗ

added theorem mv_polynomial.evalₗ_apply

added def mv_polynomial.indicator

added theorem mv_polynomial.indicator_mem_restrict_degree

added theorem mv_polynomial.ker_evalₗ

added theorem mv_polynomial.map_restrict_dom_evalₗ

added theorem mv_polynomial.range_evalᵢ

Created src/linear_algebra/finsupp.lean

added theorem cardinal_lt_omega_of_dim_lt_omega

added theorem cardinal_mk_eq_cardinal_mk_field_pow_dim

added theorem eq_bot_iff_dim_eq_zero

added theorem equiv_of_dim_eq_dim

added theorem finsupp.dim_eq

added theorem finsupp.disjoint_lsingle_lsingle

added theorem finsupp.infi_ker_lapply_le_bot

added theorem finsupp.is_basis_single

added theorem finsupp.ker_lsingle

added def finsupp.lapply

added theorem finsupp.lapply_apply

added theorem finsupp.linear_independent_single

added def finsupp.lmap_domain

added theorem finsupp.lmap_domain_apply

added def finsupp.lsingle

added theorem finsupp.lsingle_apply

added theorem finsupp.lsingle_range_le_ker_lapply

added def finsupp.lsubtype_domain

added theorem finsupp.lsubtype_domain_apply

added theorem finsupp.mem_restrict_dom

added def finsupp.restrict_dom

added def finsupp.restrict_dom_equiv_finsupp

added theorem finsupp.span_single_image

added theorem finsupp.supr_lsingle_range

added theorem injective_of_surjective

added theorem mv_polynomial.dim_mv_polynomial

added theorem mv_polynomial.is_basis_monomials

added theorem mv_polynomial.map_range_eq_map

added theorem mv_polynomial.mem_restrict_degree

added theorem mv_polynomial.mem_restrict_degree_iff_sup

added theorem mv_polynomial.mem_restrict_total_degree

added def mv_polynomial.restrict_degree

added def mv_polynomial.restrict_total_degree

Created src/linear_algebra/matrix.lean

added theorem matrix.diagonal_comp_std_basis

added theorem matrix.diagonal_to_lin

added def matrix.eval

added theorem matrix.ker_diagonal_to_lin

added theorem matrix.mul_to_lin

added theorem matrix.proj_diagonal

added theorem matrix.range_diagonal

added theorem matrix.rank_diagonal

added theorem matrix.rank_vec_mul_vec

added def matrix.to_lin

added theorem matrix.to_lin_add

added theorem matrix.to_lin_apply

added theorem matrix.to_lin_zero