Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
1 parent
96ebf8c
commit 39092ab
Showing
8 changed files
with
254 additions
and
22 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.