lean-ga icon indicating copy to clipboard operation
lean-ga copied to clipboard
verified publisher icon pygae

Some simple statements to prove

Open eric-wieser opened this issue 5 years ago • 0 comments

Just a wishlist of things I'd like to be able to prove. Feel free to add to it.

  • ∀ (Pi : Bᵣ 2) (V : Bᵣ 3), (∃ x : Bᵣ 1, x ^ Pi = V) ↔ ⟨V * Pi⟩_3 = 0 Read: a bivector lies fully within a trivector if the 3-grade part of the product is zero

eric-wieser avatar Aug 11 '20 09:08 eric-wieser