mathlib3 documentation

lean-ga / geometric_algebra.translations.ida

Derived from "A New Formalization of Origami in Geometric Algebra" #

by Tetsuo Ida, Jacques Fleuriot, and Fadoua Ghourabi

theorem ida.multivector.ext (x y : ida.multivector) (h : x.scalar = y.scalar) (h_1 : x.vector = y.vector) (h_2 : x.bivec = y.bivec) (h_3 : x.trivec = y.trivec) :
x = y

The basic abelian group operations are defined component-wise.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

scalar multiplication is also component-wise

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

We do not fully translate the multiplicative structure, as the paper does not contain it and their source code is no longer available. The content is trivial to reconstruct, but the results are uninteresting.

We continue anyway with just the important statements which the paper makes.

@[protected, instance]
Equations

Note: this declaration is incomplete and uses sorry.

@[protected, instance]
Equations

Note: this declaration is incomplete and uses sorry.

@[protected, instance]
Equations

Note: this declaration is incomplete and uses sorry.