# Commit 2019-10-22 12:22 93b17864

View on Github →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