Mathlib v3 is deprecated. Go to Mathlib v4

Theorem orientation.some_basis_orientation

Modification history

2023-03-30 18:52
src/linear_algebra/orientation.lean
refactor(linear_algebra/{multilinear,pi_tensor_product}): remove the decidable_eq argument (#10140) …
Modified orientation.some_basis_orientationView on Github →
2022-01-05 14:15
src/linear_algebra/orientation.lean
feat(linear_algebra/orientation): bases from orientations (#11234) …
Added orientation.some_basis_orientationView on Github →