mathlib

93b17864 - feat(archive): add proof of sensitivity conjecture (#1553)

feat(archive): add proof of sensitivity conjecture (#1553) * 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 * feat(archive): add proof of sensitivity conjecture * suggestions from Johan * undo removed whitespace * update header