Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 09:42 d2c5309d

View on Github →

refactor(linear_algebra/lc): use families not sets (#943)

  • refactor(linear_algebra/lc): use families not sets
  • refactor(linear_algebra/lc): merge lc into finsupp
  • refactor(linear_algebra/lc): localize decidability
  • refactor(linear_algebra/lc): finsupp instances
  • refactor(linear_algebra/lc): use families instead of sets
  • refactor(linear_algebra/lc): remove set argument in lin_indep
  • refactor(linear_algebra/lc): clean up
  • refactor(linear_algebra/lc): more clean up
  • refactor(linear_algebra/lc): set_option in section
  • refactor(linear_algebra/lc): decidability proof
  • refactor(linear_algebra/lc): arrow precedence
  • refactor(linear_algebra/lc): more cleanup
  • refactor(linear_algebra/lc): move finset.preimage
  • refactor(linear_algebra/lc): use families not sets
  • refactor(linear_algebra/lc): merge lc into finsupp
  • refactor(linear_algebra/lc): localize decidability
  • refactor(linear_algebra/lc): finsupp instances
  • refactor(linear_algebra/lc): use families instead of sets
  • refactor(linear_algebra/lc): remove set argument in lin_indep
  • refactor(linear_algebra/lc): clean up
  • refactor(linear_algebra/lc): more clean up
  • refactor(linear_algebra/lc): set_option in section
  • refactor(linear_algebra/lc): decidability proof
  • refactor(linear_algebra/lc): arrow precedence
  • refactor(linear_algebra/lc): more cleanup
  • refactor(linear_algebra/lc): move finset.preimage
  • tidying up. Remove unnecessary dec_eq from dim. Shorten finset.preimage.
  • fix build
  • make travis rebuild
  • fix build
  • shorten finsupp proofs
  • shorten more proofs
  • shorten more proofs
  • speed up dim_bot
  • fix build
  • shorten dimension proof

Estimated changes

added theorem finsupp.emb_domain_inj
added theorem finsupp.sigma_sum
added theorem finsupp.sigma_support
added theorem finsupp.single_swap
added theorem finsupp.split_apply
deleted def finsupp.to_module
deleted def finsupp.to_ring
deleted def finsupp.to_semiring
added theorem finsupp.unique_single
added theorem set.sum.elim_range
added theorem finset.coe_preimage
added theorem finset.image_preimage
added theorem finset.mem_preimage
added theorem finset.prod_preimage
modified theorem set.finite_of_finite_image
added theorem sum.elim_injective
added theorem sum.elim_inl
added theorem sum.elim_inr
added theorem submodule.linear_eq_on
modified theorem constr_add
modified theorem constr_basis
deleted theorem constr_congr
modified theorem constr_eq
modified theorem constr_neg
modified theorem constr_range
modified theorem constr_self
modified theorem constr_smul
modified theorem constr_sub
modified theorem constr_zero
modified def equiv_of_is_basis
modified theorem exists_is_basis
modified theorem exists_linear_independent
modified theorem exists_subset_is_basis
added theorem is_basis.comp
modified def is_basis.constr
modified theorem is_basis.constr_apply
modified theorem is_basis.ext
added theorem is_basis.injective
modified theorem is_basis.mem_span
modified def is_basis.repr
modified theorem is_basis.repr_eq_single
modified theorem is_basis.repr_ker
modified theorem is_basis.repr_range
deleted theorem is_basis.repr_supported
modified theorem is_basis.repr_total
modified theorem is_basis.total_comp_repr
modified theorem is_basis.total_repr
modified def is_basis
modified theorem is_basis_empty
modified theorem is_basis_empty_bot
deleted theorem is_basis_injective
modified theorem is_basis_inl_union_inr
modified theorem is_basis_singleton_one
modified theorem is_basis_span
modified theorem linear_equiv.is_basis
modified theorem linear_independent.image
modified theorem linear_independent.insert
modified theorem linear_independent.mono
modified theorem linear_independent.repr_eq
modified theorem linear_independent.repr_ker
modified theorem linear_independent.unique
modified def linear_independent
modified theorem linear_independent_empty
modified theorem linear_independent_iff
deleted def module_equiv_lc
modified theorem pi.is_basis_fun
added theorem pi.is_basis_fun₀
modified theorem pi.is_basis_std_basis
modified theorem vector_space.card_fintype'
modified theorem vector_space.card_fintype
modified theorem dim_fun'
modified theorem dim_le_injective
modified theorem dim_quotient
modified theorem dim_range_of_surjective
modified theorem dim_span
modified theorem dim_span_of_finset
added theorem dim_span_set
modified theorem exists_is_basis_fintype
modified theorem is_basis.le_span
modified theorem is_basis.mk_eq_dim
modified theorem linear_equiv.dim_eq
modified theorem linear_equiv.dim_eq_lift
modified theorem mk_eq_mk_of_basis
modified theorem rank_finset_sum_le
modified def is_basis.coord_fun
modified theorem is_basis.coord_fun_eq_repr
modified def is_basis.dual_basis
modified theorem is_basis.dual_dim_eq
deleted def is_basis.eval_lc_at
modified theorem is_basis.to_dual_apply
modified theorem is_basis.to_dual_eq_repr
modified theorem is_basis.to_dual_range
modified theorem is_basis.to_dual_to_dual
deleted theorem eq_bot_iff_dim_eq_zero
deleted theorem equiv_of_dim_eq_dim
deleted theorem finsupp.dim_eq
deleted theorem finsupp.is_basis_single
modified theorem finsupp.ker_lsingle
modified theorem finsupp.lapply_apply
modified def finsupp.lmap_domain
modified theorem finsupp.lmap_domain_apply
added theorem finsupp.lmap_domain_id
modified theorem finsupp.lsingle_apply
added def finsupp.lsum
added theorem finsupp.lsum_apply
deleted theorem finsupp.mem_restrict_dom
added theorem finsupp.mem_supported'
added theorem finsupp.mem_supported
added theorem finsupp.range_total
modified def finsupp.restrict_dom
added theorem finsupp.supported_mono
added theorem finsupp.supported_univ
added theorem finsupp.total_apply
added theorem finsupp.total_comp
added theorem finsupp.total_on_range
added theorem finsupp.total_range
added theorem finsupp.total_single
deleted theorem injective_of_surjective
added theorem eq_bot_iff_dim_eq_zero
added theorem equiv_of_dim_eq_dim
added theorem finsupp.dim_eq
deleted def lc.apply
deleted theorem lc.apply_apply
deleted theorem lc.lsum_apply
deleted theorem lc.map_apply
deleted theorem lc.map_comp
deleted theorem lc.map_disjoint_ker
deleted theorem lc.map_id
deleted theorem lc.map_supported
deleted theorem lc.map_total
deleted theorem lc.mem_supported'
deleted theorem lc.mem_supported
deleted theorem lc.range_restrict_dom
deleted def lc.restrict_dom
deleted theorem lc.restrict_dom_apply
deleted theorem lc.single_mem_supported
deleted def lc.supported
deleted theorem lc.supported_Inter
deleted theorem lc.supported_Union
deleted theorem lc.supported_comap_map
deleted theorem lc.supported_empty
deleted theorem lc.supported_mono
deleted theorem lc.supported_union
deleted theorem lc.supported_univ
deleted theorem lc.total_apply
deleted def lc.total_on
deleted theorem lc.total_on_range
deleted theorem lc.total_range
deleted theorem lc.total_single
deleted def lc
deleted theorem linear_eq_on
deleted theorem mem_span_iff_lc
deleted theorem span_eq_map_lc
added theorem nonempty_pempty
modified theorem not_nonempty_iff_imp_false
added theorem cardinal.lift_max