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

leanprover-community/mathlib,leanprover-community/mathlib