Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-21 22:57 39092ab0

View on Github →

feat(*): various lemmas from the sensitivity project (#1550)

  • feat(*): various lemmas from the sensitivity project
  • fix proof broken by nonterminal simp
  • Update src/linear_algebra/dual.lean Co-Authored-By: Johan Commelin johan@commelin.net
  • lint dual.lean
  • remove decidable_mem_of_fintype instance this leads to loops with subtype.fintype under the right decidable_eq assumptions
  • dual_lc is invalid simp lemma
  • fix namespace
  • add extra lemma
  • fix sum_const
  • remove unnecessary dec_eq assumptions
  • remove decidable_eq assumptions
  • document dual.lean
  • use classical locale
  • remove some unnecessary includes
  • remove an unused variable
  • Update src/linear_algebra/dual.lean
  • fixing a doc comment

Estimated changes

added theorem finset.sum_const'
added theorem module.smul_eq_smul
added theorem mul_ite
added theorem fintype.exists_max
added theorem set.to_finset_card
added theorem set.to_finset_inter
added def dual_pair.coeffs
added theorem dual_pair.coeffs_apply
added theorem dual_pair.coeffs_lc
added theorem dual_pair.dual_lc
added theorem dual_pair.eq_dual
added theorem dual_pair.is_basis
added def dual_pair.lc
added structure dual_pair
modified theorem is_basis.to_dual_to_dual
modified theorem cardinal.nat_cast_pow