mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

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

Open hrmacbeth opened this issue 3 years ago • 1 comments

Construction of the cross-product on an oriented real inner product space of dimension 3.

Formalized as part of the Sphere Eversion project.

Open in Gitpod

  • [x] depends on: #16475
  • [x] depends on: #16476
  • [x] depends on: #16477
  • [x] depends on: #16478
  • [x] depends on: #16479
  • [x] depends on: #16487

hrmacbeth avatar Sep 12 '22 22:09 hrmacbeth

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16475~~
  • ~~leanprover-community/mathlib#16476~~
  • ~~leanprover-community/mathlib#16477~~
  • ~~leanprover-community/mathlib#16478~~
  • ~~leanprover-community/mathlib#16479~~
  • ~~leanprover-community/mathlib#16487~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 12 '22 14:10 mathlib-dependent-issues-bot