lean-ga
lean-ga copied to clipboard
pygae
A partial formalization of Geometric Algebra in the Lean formal proof verification system.
This is now fully covered by https://github.com/leanprover-community/mathlib4/pull/6778
For now, we probably want to build on top of this limited to ℕ anyway. This does not build any more...
Moved from #1, this is easier to look at as a PR. The payoff of all this is that ```lean parameter v : G₁ -- Addition! #check ((2 + v)...
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...
Some discussion at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Ideals.20over.20algebras