mathlib3
feat(analysis/inner_product_space/cross_product): general construction of the cross-product
#16490
Open
Overview
Commits
56
Changes
View On GitHub

feat(analysis/inner_product_space/cross_product): general construction of the cross-product #16490

hrmacbeth wants to merge 56 commits into master from new-cross-product
hrmacbeth
hrmacbeth test ci
9c871d57
hrmacbeth test ci
bc475b5f
hrmacbeth test ci
0575ee6c
hrmacbeth oriented_angle
e2ecd04b
hrmacbeth fix
9e9c68fa
hrmacbeth test ci
99079cec
hrmacbeth test ci
6e809e22
hrmacbeth long line
8541edf0
hrmacbeth test ci
14a53ceb
hrmacbeth fix
03b0ec80
hrmacbeth namespaces
d82a742f
hrmacbeth fix name
6a220659
hrmacbeth fix
2105bd19
hrmacbeth Merge branch 'det_adjust_to_orientation' into volume-form
9b8a1f10
hrmacbeth Merge branch 'gram_schmidt_orthonormal_basis' into volume-form
c74d97c5
hrmacbeth Merge branch 'orthonormal_basis_adjust_orientation' into volume-form
f2fb3264
hrmacbeth Merge branch 'unitary_change_of_basis' into volume-form
dd1fbe8f
hrmacbeth fix
403502c7
hrmacbeth Merge branch 'extend_orthonormal_fixed_index' into gram_schmidt_ortho…
7461a727
hrmacbeth fix
afea4284
hrmacbeth Update src/linear_algebra/orientation.lean
c04152f4
hrmacbeth Merge branch 'det_adjust_to_orientation' into volume-form
68061311
hrmacbeth Merge branch 'extend_orthonormal_fixed_index' into volume-form
a88ab532
hrmacbeth fix namespacing
9fdb865c
hrmacbeth Merge branch 'det_adjust_to_orientation' into volume-form
699721dc
hrmacbeth volume form
21959eb7
hrmacbeth lint
a3e628fd
hrmacbeth cross product
ef160f39
hrmacbeth hrmacbeth added awaiting-CI
hrmacbeth hrmacbeth added t-analysis
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
github-actions github-actions removed awaiting-CI
hrmacbeth Merge remote-tracking branch 'origin/master' into volume-form
bae31a90
hrmacbeth Merge remote-tracking branch 'origin/master' into extend_orthonormal_…
8e2a1d01
hrmacbeth Merge branch 'extend_orthonormal_fixed_index' into volume-form
f912aeaf
hrmacbeth lemma renamed
29f59854
hrmacbeth Merge branch 'extend_orthonormal_fixed_index' into volume-form
00851a9b
hrmacbeth Merge remote-tracking branch 'origin/master' into gram_schmidt_orthon…
97c6fc99
hrmacbeth long line
16b457c8
hrmacbeth Merge branch 'gram_schmidt_orthonormal_basis' into volume-form
c2c2c4b6
hrmacbeth Merge branch 'volume-form' into new-cross-product
eee72994
hrmacbeth fix
a046e016
hrmacbeth Merge remote-tracking branch 'origin/master' into volume-form
3e3c6ba8
hrmacbeth Merge branch 'volume-form' into new-cross-product
5ebc15aa
hrmacbeth docs
1addc402
hrmacbeth make lemma iff
f1af9b07
hrmacbeth change notation
5fc7d55e
hrmacbeth drop succ condition
320e8033
hrmacbeth lint
f8979907
hrmacbeth irreducible attribute
196b63aa
hrmacbeth Update src/linear_algebra/orientation.lean
ca302993
hrmacbeth classify "orientations" wrt empty type
5db1287e
hrmacbeth fix
c9608bf5
hrmacbeth fix main file
1ba50081
hrmacbeth Merge remote-tracking branch 'origin/master' into volume-form
96f2e180
hrmacbeth Merge branch 'volume-form' into new-cross-product
4beca947
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
hrmacbeth hrmacbeth added awaiting-review
mcdoll
mcdoll commented on 2022-10-13
hrmacbeth copy conventions from area_form file
387a09dd
hrmacbeth swap lemma
a54f5902
mcdoll
mcdoll commented on 2022-10-13
hrmacbeth Update src/analysis/inner_product_space/cross_product.lean
5b51aec5
hrmacbeth fix
41bf0bb7
ocfnash
ocfnash commented on 2022-10-20
ocfnash ocfnash removed awaiting-review
ocfnash ocfnash added awaiting-author
ocfnash ocfnash added t-algebra
ocfnash ocfnash removed t-analysis
mcdoll
mcdoll commented on 2022-10-25
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-author t-algebra too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum