Derived from "A New Formalization of Origami in Geometric Algebra" #
by Tetsuo Ida, Jacques Fleuriot, and Fadoua Ghourabi
@[ext]
Instances for ida.multivector
- ida.multivector.has_sizeof_inst
- ida.multivector.has_zero
- ida.multivector.has_add
- ida.multivector.has_sub
- ida.multivector.has_neg
- ida.multivector.add_comm_group
- ida.multivector.has_smul
- ida.multivector.module
- ida.multivector.has_one
- ida.multivector.has_mul
- ida.multivector.ring
- ida.multivector.algebra
The basic abelian group operations are defined component-wise.
@[protected, instance]
@[protected, instance]
Equations
- ida.multivector.add_comm_group = {add := has_add.add ida.multivector.has_add, add_assoc := ida.multivector.add_comm_group._proof_1, zero := 0, zero_add := ida.multivector.add_comm_group._proof_2, add_zero := ida.multivector.add_comm_group._proof_3, nsmul := add_group.nsmul._default 0 has_add.add ida.multivector.add_comm_group._proof_4 ida.multivector.add_comm_group._proof_5, nsmul_zero' := ida.multivector.add_comm_group._proof_6, nsmul_succ' := ida.multivector.add_comm_group._proof_7, neg := has_neg.neg ida.multivector.has_neg, sub := has_sub.sub ida.multivector.has_sub, sub_eq_add_neg := ida.multivector.add_comm_group._proof_8, zsmul := add_group.zsmul._default has_add.add ida.multivector.add_comm_group._proof_9 0 ida.multivector.add_comm_group._proof_10 ida.multivector.add_comm_group._proof_11 (add_group.nsmul._default 0 has_add.add ida.multivector.add_comm_group._proof_4 ida.multivector.add_comm_group._proof_5) ida.multivector.add_comm_group._proof_12 ida.multivector.add_comm_group._proof_13 has_neg.neg, zsmul_zero' := ida.multivector.add_comm_group._proof_14, zsmul_succ' := ida.multivector.add_comm_group._proof_15, zsmul_neg' := ida.multivector.add_comm_group._proof_16, add_left_neg := ida.multivector.add_comm_group._proof_17, add_comm := ida.multivector.add_comm_group._proof_18}
scalar multiplication is also component-wise
@[protected, instance]
Equations
- ida.multivector.module = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := has_smul.smul ida.multivector.has_smul}, one_smul := ida.multivector.module._proof_1, mul_smul := ida.multivector.module._proof_2}, smul_zero := ida.multivector.module._proof_3, smul_add := ida.multivector.module._proof_4}, add_smul := ida.multivector.module._proof_5, zero_smul := ida.multivector.module._proof_6}
@[protected, instance]
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
- ida.multivector.ring = sorry
Note: this declaration is incomplete and uses sorry.
@[protected, instance]
Equations
- ida.multivector.algebra = sorry
Note: this declaration is incomplete and uses sorry.