Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(linear_algebra): generalize conversion between matrices and bil…
…inear forms to semirings (#14263) Only one lemma was moved (`dual_distrib_apply`), none were renamed, and no proofs were meaningfully changed. Section markers were shuffled around, and some variables exchanged for variables with weaker typeclass assumptions. A few other things have been generalized to semiring at the same time; `linear_map.trace` and `linear_map.smul_rightₗ`
- Loading branch information
1 parent
e09e877
commit cef5898
Showing
9 changed files
with
131 additions
and
112 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.