-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - feat(linear_algebra/*): Use alternating maps for wedge and determinant #5124
Conversation
/-- The product of `n` terms of the form `ι R m` is an alternating map. | ||
|
||
This is a special case of `multilinear_map.mk_pi_algebra_fin` -/ | ||
def ι_multi (n : ℕ) : |
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'm not really sure what a good name for this is. wedge
is another option, but it's weird that we use *
as the symbol for a product that we call a wedge product.
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.
The name looks fine to me right now, since it's the (alternating) multilinear version of ι
.
1b54b47
to
b2a4fa8
Compare
src/linear_algebra/matrix.lean
Outdated
map_eq_zero_of_eq' := begin | ||
intros v i j h hij, | ||
rw [←function.update_eq_self i v, h, ←det_transpose, he.to_matrix_update, ←update_row_transpose], | ||
have : (he.to_matrix v)ᵀ j = he.repr (v j) := funext (λ _, rfl), |
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.
Zulip thread about whether this lemma should have a name.
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.
Seeing in this context, I believe it should have a name, but probably not be a simp
lemma.
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.
Looks good to me if you can extract that to_matrix_transpose
lemma.
bors d+
src/linear_algebra/matrix.lean
Outdated
map_eq_zero_of_eq' := begin | ||
intros v i j h hij, | ||
rw [←function.update_eq_self i v, h, ←det_transpose, he.to_matrix_update, ←update_row_transpose], | ||
have : (he.to_matrix v)ᵀ j = he.repr (v j) := funext (λ _, rfl), |
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.
Seeing in this context, I believe it should have a name, but probably not be a simp
lemma.
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
3cea314
to
9565c2c
Compare
bors r+ |
…nt (#5124) This : * Adds `exterior_algebra.ι_multi`, where `ι_multi ![a, b ,c]` = `ι a * ι b * ι c` * Makes `det_row_multilinear` an `alternating_map` * Makes `is_basis.det` an `alternating_map`
Pull request successfully merged into master. Build succeeded: |
This :
exterior_algebra.ι_multi
, whereι_multi ![a, b ,c]
=ι a * ι b * ι c
det_row_multilinear
analternating_map
is_basis.det
analternating_map
I think
ι_multi
is was what @zhangir-azerbayev was preparing to prove after they wrapped up #3770