Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(linear_algebra): Matrix inverses for square nonsingular matrices #1816
feat(linear_algebra): Matrix inverses for square nonsingular matrices #1816
Changes from all commits
d5425cc
d49a280
c508497
bf3eaa6
9196a21
a50c72a
1ae96a6
802c4ec
f91d847
9242b03
db49d64
d146ead
078d28b
06d5e1f
0176199
a605cb0
59f65c8
867feb3
7d6f5fc
7d32651
ea9be5e
fbd8af6
0ead3d4
bfdc2cd
bfccd9e
d5ccd12
8057b7c
6bc4b7a
b02933a
1cc4827
d0c0d38
b9b5d1b
1e163a9
608f853
21d6b55
7a275ab
9dc30e9
3a44403
7cdd1f4
9a065c8
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is the same as quotienting by the subgroup generated by
swap i j
. This is probably a nicer statement.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried rewording the statement, but unfortunately it seems like the original version is easier to work with.
The argument I want to use is that the determinant is a sum adding up to
0
because the term corresponding toσ
cancels with the term corresponding toswap i j * σ
. Thus, I want to partition the permutations so that the classes are{σ, swap i j * σ}
, and then the sum over this class isx + -1 * x + 0 = 0
.Using the quotient of
group.closure {swap i j}
would then require as a first step showing that the classes are{σ, swap i j * σ}
, which was immediate from the originalmod_swap
definition. (Is there a better way to showquotient_group.left_rel (group.closure {swap i j}) σ τ ↔ (σ = τ ∨ σ = swap i j * τ)
than first usinggroup.closure {swap i j} = gpowers (swap i j) = {σ // ∃ k, σ = (swap i j)^k}
, then showing(∃ k, σ = (swap i j)^k) ↔ (∃ 0 ≤ k < order_of (swap i j), σ = (swap i j)^k) ↔ (σ = id ∨ σ = swap i j)
?) So I don't expect the change is really worth the extra work.