mathlib

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

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