Theorems · Theorem · combinatorics
Configuration.ofField.crossProduct_eq_zero_of_dotProduct_eq_zero
∀ {K : Type u_3} [inst : Field K] {a b c d : Fin 3 → K},
a ⬝ᵥ c = 0 → b ⬝ᵥ c = 0 → a ⬝ᵥ d = 0 → b ⬝ᵥ d = 0 → (crossProduct a) b = 0 ∨ (crossProduct c) d = 0- Defined in
- Mathlib.Combinatorics.Configuration
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Fieldstatement and proof · cited by 7,404
- Matrixproof · cited by 4,303
- Fintype.cardproof · cited by 1,386
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- LinearIndependentproof · cited by 560
- Matrix.extproof · cited by 540
- Matrix.transposeproof · cited by 389
- Matrix.ofproof · cited by 336
Cited by1
Results whose statement or proof uses this declaration.
- Configuration.ofField.eq_or_eq_of_orthogonalproof · cited by 0