Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-06 12:45 a5fa162b

View on Github →

chore(data/mv_polynomial): use classical logic (#1391)

  • 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
  • make data.finsupp classical
  • trouble with data/polynomial
  • ...
  • more classical
  • merge
  • merge
  • merge
  • fix
  • removing more
  • minor
  • ?
  • progress, using convert
  • working?
  • remove some unnecessary converts
  • fixes
  • err
  • oops
  • various
  • various
  • fix free_comm_ring
  • remove test lines
  • fix linear_algebra/matrix.lean
  • Fix errors in power_series.lean
  • trying to turn instances back on
  • restore some instances
  • no joy
  • fix mv_polynomial errors
  • another convert

Estimated changes

modified theorem finsupp.comap_domain_apply
modified theorem finsupp.count_to_multiset
modified def finsupp.filter
modified theorem finsupp.filter_curry
modified theorem finsupp.filter_smul
modified theorem finsupp.map_domain_smul
modified theorem finsupp.map_range_add
modified theorem finsupp.mem_support_single
modified def finsupp.of_multiset
modified theorem finsupp.of_multiset_apply
modified theorem finsupp.prod_single
modified theorem finsupp.single_finset_sum
modified theorem finsupp.single_multiset_sum
modified theorem finsupp.single_sum
modified theorem finsupp.single_swap
modified theorem finsupp.smul_single
modified theorem finsupp.sum_comap_domain
modified theorem finsupp.support_curry
modified theorem finsupp.support_eq_empty
modified theorem finsupp.support_subset_iff
modified theorem mv_polynomial.coeff_zero_X
modified theorem mv_polynomial.degrees_prod
modified theorem mv_polynomial.degrees_sum
modified theorem mv_polynomial.degrees_zero
modified theorem mv_polynomial.eval_assoc
modified theorem mv_polynomial.eval₂_assoc
modified theorem mv_polynomial.eval₂_hom_X
modified theorem mv_polynomial.eval₂_prod
modified theorem mv_polynomial.eval₂_sum
modified theorem mv_polynomial.map_eval₂
modified theorem mv_polynomial.map_map
modified theorem mv_polynomial.rename_sub
modified theorem polynomial.coeff_C_zero
modified theorem polynomial.coeff_X
modified theorem polynomial.coeff_X_one
modified theorem polynomial.coeff_X_zero
modified theorem polynomial.coeff_one
modified theorem polynomial.coeff_one_zero
modified theorem polynomial.coeff_single
modified theorem polynomial.coeff_sum
modified theorem polynomial.degree_map'
modified theorem polynomial.degree_map_le
modified theorem polynomial.degree_sum_le
modified theorem polynomial.map_div_by_monic
modified theorem polynomial.map_map
modified theorem polynomial.map_mod_by_monic
modified theorem polynomial.map_neg
modified theorem polynomial.map_sub
modified theorem polynomial.monic_map
modified theorem polynomial.nat_degree_map'
modified def finsupp.lsum
modified theorem finsupp.lsum_apply
modified theorem finsupp.range_restrict_dom
modified def finsupp.restrict_dom
modified theorem finsupp.restrict_dom_apply
modified theorem finsupp.is_basis_single
modified theorem power_series.coeff_mk
modified theorem power_series.coeff_trunc
modified theorem power_series.monomial_zero
modified def power_series.trunc
modified theorem power_series.trunc_C
modified theorem power_series.trunc_add
modified theorem power_series.trunc_one
modified theorem power_series.trunc_zero