# Formalisation of Geometric Algebras

Coq8.3 archive GeometricAlgebra.zip

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1305 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (700 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (145 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (226 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (110 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |

# Global Index

## A

action [inductive, in tuple3]addE [projection, in VectorSpace]

addE_com [projection, in VectorSpace]

addE_assoc [projection, in VectorSpace]

addE_cancell [lemma, in VectorSpace]

addE_mprod [lemma, in VectorSpace]

addE_eq_opp [lemma, in VectorSpace]

addE_swap [lemma, in VectorSpace]

addE_cancelr [lemma, in VectorSpace]

addE0l [projection, in VectorSpace]

addE0r [lemma, in VectorSpace]

addk [lemma, in Grassmann]

addK [projection, in Field]

addK_assoc [projection, in Field]

addK_com [projection, in Field]

addK_cancel [lemma, in Field]

addK_eq_opp [lemma, in Field]

addK0l [projection, in Field]

addK0r [lemma, in Field]

add_multKr [lemma, in Field]

add_multKl [projection, in Field]

add_hom [lemma, in Grassmann]

all [definition, in Grassmann]

all_prods_lift [lemma, in Grassmann]

all_prods_free [lemma, in Grassmann]

all_prods_cons [lemma, in Grassmann]

all_hom1 [definition, in Grassmann]

all_hom1_cor [lemma, in Grassmann]

all_hom [lemma, in Grassmann]

all_prods_length [lemma, in Grassmann]

all_prods_id [lemma, in Grassmann]

all_prods1 [lemma, in Grassmann]

all_prods_hom [lemma, in Grassmann]

all_prods_nil [lemma, in Grassmann]

andbP [lemma, in Aux]

Aux [library]

## B

base [definition, in Grassmann]base_nil [lemma, in Grassmann]

base_lift [lemma, in Grassmann]

base_free [lemma, in Grassmann]

base_in [lemma, in Grassmann]

base_length [lemma, in Kn]

base_length [lemma, in Grassmann]

base_n [lemma, in Grassmann]

base_hom [lemma, in Grassmann]

base_lt_nil [lemma, in Grassmann]

base_free [lemma, in Kn]

base0 [lemma, in Grassmann]

base1_length [lemma, in Grassmann]

base1_S [lemma, in Grassmann]

bin [definition, in Aux]

bin_def [lemma, in Aux]

bin_more [lemma, in Aux]

bin_0 [lemma, in Aux]

bin_nn [lemma, in Aux]

bin_1 [lemma, in Aux]

bracket [definition, in G3]

bracket_defE [lemma, in G3]

bracket_defr [lemma, in G3]

bracket_norm [lemma, in G3]

bracket_free [lemma, in G3]

bracket_swapl [lemma, in G3]

bracket_swapr [lemma, in G3]

bracket_defl [lemma, in G3]

bracket_expand [lemma, in G3]

bracket0l [lemma, in G3]

bracket0m [lemma, in G3]

bracket0r [lemma, in G3]

bracket0_collinear [lemma, in G3]

b2Prop [definition, in Aux]

b2PropT [lemma, in Aux]

## C

cadd [definition, in tuple3]cadd_opp [lemma, in tuple3]

cadd_c [lemma, in tuple3]

cbl [inductive, in Grassmann]

cbl [inductive, in VectorSpace]

cblk_homk_equiv [lemma, in Grassmann]

cblnil [lemma, in VectorSpace]

cbl_incl [lemma, in VectorSpace]

cbl_joinl0_mprod [lemma, in Grassmann]

cbl_join_com [lemma, in Grassmann]

cbl_add [constructor, in Grassmann]

cbl_join [constructor, in Grassmann]

cbl_all_prods [lemma, in Grassmann]

cbl_hom [lemma, in Grassmann]

cbl_joinl0 [lemma, in Grassmann]

cbl_base1_list_split [lemma, in Grassmann]

cbl_scal [constructor, in Grassmann]

cbl_in [constructor, in VectorSpace]

cbl_map_inv [lemma, in VectorSpace]

cbl_base_join_com [lemma, in Grassmann]

cbl_contra [lemma, in Grassmann]

cbl_mprod [lemma, in VectorSpace]

cbl_base [lemma, in Kn]

cbl_mcontra [lemma, in Grassmann]

cbl_base1_split [lemma, in Grassmann]

cbl_map [lemma, in VectorSpace]

cbl_trans [lemma, in VectorSpace]

cbl_in [constructor, in Grassmann]

cbl_scal [constructor, in VectorSpace]

cbl_cons [lemma, in Grassmann]

cbl_join_id [lemma, in Grassmann]

cbl_base_join_id [lemma, in Grassmann]

cbl_joinl [lemma, in Grassmann]

cbl_add [constructor, in VectorSpace]

cbl0 [constructor, in VectorSpace]

cbl0_inv [lemma, in VectorSpace]

cbl1 [lemma, in VectorSpace]

cbl1_hom1_equiv [lemma, in Grassmann]

ccmp [definition, in tuple3]

ccons [definition, in tuple3]

ccons_c [lemma, in tuple3]

cdual [definition, in Clifford]

cdual_cliff [lemma, in Clifford]

Clifford [library]

cliff_star [definition, in Clifford]

cliff_starb [definition, in Clifford]

coef [definition, in tuple3]

collinear [definition, in G3]

collinear_bracket [lemma, in G3]

collinear_bracket0 [lemma, in G3]

concur [definition, in G3]

conep [definition, in tuple3]

conep_c [lemma, in tuple3]

conjf_meetl [lemma, in Grassmann]

conjf_hom [lemma, in Grassmann]

conjf_prod_scal [lemma, in Clifford]

conjf_meetr [lemma, in Grassmann]

conjf_gprod [lemma, in Clifford]

conjf_join [lemma, in Grassmann]

conjk [lemma, in Grassmann]

conjt [lemma, in Grassmann]

conjt_hom [lemma, in Grassmann]

conj_scal [lemma, in Grassmann]

conj_swap [lemma, in Grassmann]

conj_add [lemma, in Grassmann]

conj_dual [lemma, in Grassmann]

conj_hom [lemma, in Grassmann]

conj_all [lemma, in Grassmann]

conj_neg [lemma, in Grassmann]

conj_const [lemma, in Grassmann]

conj_dconst [lemma, in Grassmann]

conj_e [lemma, in Grassmann]

conj_invo [lemma, in Grassmann]

conj0 [lemma, in Grassmann]

const [definition, in Grassmann]

constk [lemma, in Grassmann]

const_scal [lemma, in Grassmann]

const_add [lemma, in Grassmann]

const_hom [lemma, in Grassmann]

const_dual [lemma, in Grassmann]

const_join [lemma, in Grassmann]

const0 [lemma, in Grassmann]

const1 [lemma, in G3]

contraction_rule [definition, in tuple3]

contraction_v3 [lemma, in G3]

contraction_v2 [lemma, in G3]

contraction_rule_c [lemma, in tuple3]

contraction_v1 [lemma, in G3]

contraction_v0 [lemma, in G3]

contraE [lemma, in Grassmann]

contrak [lemma, in Grassmann]

contra_join [lemma, in Grassmann]

contra_scall [lemma, in Grassmann]

contra_const [lemma, in Grassmann]

contra_id [lemma, in Grassmann]

contra_hom0 [lemma, in Grassmann]

contra_swap [lemma, in Grassmann]

contra_e [lemma, in Grassmann]

contra_addl [lemma, in Grassmann]

contra_conj [lemma, in Grassmann]

contra_addr [lemma, in Grassmann]

contra_scalr [lemma, in Grassmann]

contra_hom [lemma, in Grassmann]

contra0l [lemma, in Grassmann]

contra0r [lemma, in Grassmann]

copp [definition, in tuple3]

copp_c [lemma, in tuple3]

cscale [definition, in tuple3]

cscale_c [lemma, in tuple3]

czerop [definition, in tuple3]

czerop_opp [lemma, in tuple3]

czerop_c [lemma, in tuple3]

c0 [definition, in tuple3]

c0_c [lemma, in tuple3]

c1 [definition, in tuple3]

c1_c [lemma, in tuple3]

## D

dconjf_meetd [lemma, in Grassmann]dconjf_joinr [lemma, in Grassmann]

dconjf_hom [lemma, in Grassmann]

dconjf_meet [lemma, in Grassmann]

dconjf_joinl [lemma, in Grassmann]

dconjk [lemma, in Grassmann]

dconjt [lemma, in Grassmann]

dconjt_hom [lemma, in Grassmann]

dconj_const [lemma, in Grassmann]

dconj_dual [lemma, in Grassmann]

dconj_all [lemma, in Grassmann]

dconj_scal [lemma, in Grassmann]

dconj_conj_swap [lemma, in Grassmann]

dconj_conj [lemma, in Grassmann]

dconj_swap [lemma, in Grassmann]

dconj_neg [lemma, in Grassmann]

dconj_dconst [lemma, in Grassmann]

dconj_hom [lemma, in Grassmann]

dconj_add [lemma, in Grassmann]

dconj_invo [lemma, in Grassmann]

dconj0 [lemma, in Grassmann]

dconst [definition, in Grassmann]

dconst_dual [lemma, in Grassmann]

dconst_meet [lemma, in Grassmann]

dconst_scal [lemma, in Grassmann]

dconst_all [lemma, in Grassmann]

dconst_add [lemma, in Grassmann]

dconst_hom [lemma, in Grassmann]

dconst0 [lemma, in Grassmann]

deck0 [lemma, in Grassmann]

decomposable [definition, in Grassmann]

decomposable_factor [lemma, in Grassmann]

decompose [definition, in Grassmann]

decomposek [definition, in Grassmann]

decomposekSS [lemma, in Grassmann]

decomposek_cor [lemma, in Grassmann]

decompose_cor [lemma, in Grassmann]

decomp_hom [lemma, in Grassmann]

decomp_one_factor0 [lemma, in Grassmann]

decomp_cbl [lemma, in Grassmann]

decomp_one_factor_hom [lemma, in Grassmann]

decomp_one_factor_join [lemma, in Grassmann]

delta [definition, in tuple3]

delta_c [lemma, in tuple3]

Desargues [lemma, in G3]

dhead [definition, in Aux]

dim [projection, in VectorSpace]

div2_prop [lemma, in Aux]

div2_double_p [lemma, in Aux]

dlift [definition, in Grassmann]

dlift_mprod [lemma, in Grassmann]

dlift_scal [lemma, in Grassmann]

dlift_add [lemma, in Grassmann]

dmap2_eql [lemma, in Kn]

do_auto [definition, in tuple3]

do_auto_c [lemma, in tuple3]

do_elim_c [lemma, in tuple3]

do_elim [definition, in tuple3]

do_contra_c [lemma, in tuple3]

do_contra [definition, in tuple3]

do_free_c [lemma, in tuple3]

do_free [definition, in tuple3]

dual [definition, in Grassmann]

dualE [lemma, in Clifford]

dualk [lemma, in Grassmann]

dual_hom [lemma, in Grassmann]

dual_base [lemma, in Grassmann]

dual_invoE [lemma, in Grassmann]

dual_invoE [lemma, in G3]

dual_invo [lemma, in Grassmann]

dual_meet [lemma, in Grassmann]

dual_add [lemma, in Grassmann]

dual_join [lemma, in Grassmann]

dual_scal [lemma, in Grassmann]

dual_join_compl [lemma, in Grassmann]

dual_all [lemma, in Grassmann]

dual0 [lemma, in Grassmann]

dual0E [lemma, in Grassmann]

dual1 [lemma, in Grassmann]

## E

E [abbreviation, in Clifford]E [projection, in VectorSpace]

ecompare [definition, in tuple3]

edelta [definition, in tuple3]

edelta_c [lemma, in tuple3]

edelta_in [lemma, in tuple3]

einsert [definition, in tuple3]

einsert_length [lemma, in tuple3]

einsert_c [lemma, in tuple3]

einsert0 [definition, in tuple3]

einsert0_c [lemma, in tuple3]

elsprod [definition, in tuple3]

en_def [lemma, in Grassmann]

eparams [record, in VectorSpace]

eqE [projection, in VectorSpace]

eqE_spec [lemma, in VectorSpace]

eqE_refl [lemma, in VectorSpace]

eqE_dec [projection, in VectorSpace]

eqK [projection, in Field]

eqKI [lemma, in Field]

eqK_dec [projection, in Field]

eqK_spec [lemma, in Field]

eql_t0Nr [constructor, in Kn]

eql_t0Nl [constructor, in Kn]

eql_t0 [inductive, in Kn]

eql_sym [lemma, in Kn]

eql_refl [lemma, in Kn]

eql_trans [lemma, in Kn]

eql_t0N [constructor, in Kn]

eql_t0R [constructor, in Kn]

eq_natP [lemma, in Aux]

eq_nat [definition, in Aux]

eq_nat_spec [inductive, in Aux]

eq_Spect [constructor, in Aux]

eq_nat_specb [constructor, in Aux]

eq_Specf [constructor, in Aux]

eq_nat_spect [constructor, in Aux]

eq_Spec [inductive, in Aux]

eq0I [lemma, in Grassmann]

eq0_dec [lemma, in Grassmann]

eq0_spec [lemma, in Grassmann]

eremove [definition, in tuple3]

eremove_c [lemma, in tuple3]

esprod [definition, in tuple3]

etsort [definition, in tuple3]

etsort_c [lemma, in tuple3]

Exp [section, in Aux]

expand_meetr [lemma, in G3]

expand_meetl [lemma, in G3]

expKm1_2E [lemma, in Field]

expKm1_sub [lemma, in Field]

expKm1_odd [lemma, in Field]

expKm1_n0 [lemma, in Field]

expKm1_2 [lemma, in Field]

expKm1_even [lemma, in Field]

expKS [lemma, in Field]

expK_add [lemma, in Field]

expK_integral [lemma, in Field]

expK2m1 [lemma, in Field]

expS [lemma, in Aux]

exp0 [lemma, in Aux]

ex1_proof [lemma, in tuple3]

ex10_proof1 [lemma, in tuple3]

ex10_proof2 [lemma, in tuple3]

ex11_proof [lemma, in tuple3]

ex12_proof [lemma, in tuple3]

ex13_proof [lemma, in tuple3]

ex14_proof [lemma, in tuple3]

ex15_proof [lemma, in tuple3]

ex16_proof [lemma, in tuple3]

ex17_proof [lemma, in tuple3]

ex18_proof [lemma, in tuple3]

ex19_proof [lemma, in tuple3]

Ex2D [module, in Grassmann]

Ex2D.p [variable, in Grassmann]

Ex2D.X [definition, in Grassmann]

Ex2D.Y [definition, in Grassmann]

_ ∨ _ [notation, in Grassmann]

_ + _ [notation, in Grassmann]

_ ∧ _ [notation, in Grassmann]

_ .* _ [notation, in Grassmann]

'@ _ [notation, in Grassmann]

[[ X: _ , Y: _ , X**Y: _ ]] [notation, in Grassmann]

ex2_proof [lemma, in tuple3]

ex20_proof [lemma, in tuple3]

ex21_proof [definition, in tuple3]

Ex3D [module, in Grassmann]

Ex3D.p [variable, in Grassmann]

Ex3D.X [definition, in Grassmann]

Ex3D.Y [definition, in Grassmann]

Ex3D.Z [definition, in Grassmann]

_ ∧ _ [notation, in Grassmann]

_ + _ [notation, in Grassmann]

_ .* _ [notation, in Grassmann]

_ ∨ _ [notation, in Grassmann]

'@ _ [notation, in Grassmann]

[[ X: _ , Y: _ , Z: _ , X**Y: _ , Y**Z: _ , X**Z: _ , X**Y**Z: _ ]] [notation, in Grassmann]

ex3_proof [lemma, in tuple3]

Ex4D [module, in Grassmann]

Ex4D.fxt [definition, in Grassmann]

Ex4D.fxy [definition, in Grassmann]

Ex4D.fxz [definition, in Grassmann]

Ex4D.fyt [definition, in Grassmann]

Ex4D.fyz [definition, in Grassmann]

Ex4D.fzt [definition, in Grassmann]

Ex4D.p [variable, in Grassmann]

Ex4D.T [definition, in Grassmann]

Ex4D.T' [definition, in Grassmann]

Ex4D.U [definition, in Grassmann]

Ex4D.X [definition, in Grassmann]

Ex4D.X' [definition, in Grassmann]

Ex4D.Y [definition, in Grassmann]

Ex4D.Y' [definition, in Grassmann]

Ex4D.Z [definition, in Grassmann]

Ex4D.Z' [definition, in Grassmann]

_ ∧ _ [notation, in Grassmann]

_ ∨ _ [notation, in Grassmann]

_ + _ [notation, in Grassmann]

_ .* _ [notation, in Grassmann]

#< _ , _ ># [notation, in Grassmann]

'@ _ [notation, in Grassmann]

[[ X: _ , Y: _ , Z: _ , T: _ , X**Y: _ , X**Z: _ , X**T: _ , Y**Z: _ , Y**T: _ , Z**T: _ , X**Y**Z: _ , X**Y**T: _ , X**Z**T: _ , Y**Z**T: _ , X**Y**Z**T: _ , K: _ ]] [notation, in Grassmann]

ex4_proof [lemma, in tuple3]

Ex5D [module, in Grassmann]

Ex5D.p [variable, in Grassmann]

Ex5D.T [definition, in Grassmann]

Ex5D.U [definition, in Grassmann]

Ex5D.X [definition, in Grassmann]

Ex5D.Y [definition, in Grassmann]

Ex5D.Z [definition, in Grassmann]

_ ∧ _ [notation, in Grassmann]

_ .* _ [notation, in Grassmann]

_ ∨ _ [notation, in Grassmann]

_ + _ [notation, in Grassmann]

'@ _ [notation, in Grassmann]

[[ X: _ , Y: _ , Z: _ , T: _ , U: _ , X**Y: _ , X**Z: _ , X**T: _ , X**U: _ , Y**Z: _ , Y**T: _ , Y**U: _ , Z**T: _ , Z**U: _ , T**U: _ , X**Y**Z: _ , X**Y**T: _ , X**Y**U: _ , X**Z**T: _ , X**Z**U: _ , X**T**U: _ , Y**Z**T: _ , Y**Z**U: _ , Y**T**U: _ , Z**T**U: _ , X**Y**Z**T: _ , X**Y**Z**U: _ , X**Y**T**U: _ , X**Z**T**U: _ , Y**Z**T**U: _ , X**Y**Z**T**U: _ , K: _ ]] [notation, in Grassmann]

ex5_l [lemma, in tuple3]

Ex6D [module, in Grassmann]

Ex6D.K [definition, in Grassmann]

Ex6D.p [variable, in Grassmann]

Ex6D.T [definition, in Grassmann]

Ex6D.U [definition, in Grassmann]

Ex6D.X [definition, in Grassmann]

Ex6D.Y [definition, in Grassmann]

Ex6D.Z [definition, in Grassmann]

_ .* _ [notation, in Grassmann]

_ ∧ _ [notation, in Grassmann]

_ ∨ _ [notation, in Grassmann]

_ + _ [notation, in Grassmann]

'@ _ [notation, in Grassmann]

ex6_proof [lemma, in tuple3]

ex7_proof [definition, in tuple3]

ex8_proof [lemma, in tuple3]

ex9_proof3 [lemma, in tuple3]

ex9_proof1 [lemma, in tuple3]

ex9_proof2 [lemma, in tuple3]

e_in_base [lemma, in Kn]

e_in_base_ex [lemma, in Kn]

e_in_base1_ex [lemma, in Grassmann]

e_in_base1 [lemma, in Grassmann]

E0 [projection, in VectorSpace]

## F

f [definition, in Grassmann]f [definition, in Kn]

factor [definition, in Grassmann]

factork [lemma, in Grassmann]

factor_hom [lemma, in Grassmann]

factor_scal [lemma, in Grassmann]

factor_add [lemma, in Grassmann]

factor_ortho [lemma, in Grassmann]

factor_factor [lemma, in Grassmann]

factor_hom0E [lemma, in Grassmann]

factor_id [lemma, in Grassmann]

factor0 [lemma, in Grassmann]

factor0_hom0 [lemma, in Grassmann]

fbracket [definition, in G3]

fbracket_norm [lemma, in G3]

felim [definition, in tuple3]

felim_c [lemma, in tuple3]

FF [section, in tuple3]

FF.Examples [section, in tuple3]

FF.Examples.ex1 [variable, in tuple3]

FF.Examples.ex10_2 [variable, in tuple3]

FF.Examples.ex10_1 [variable, in tuple3]

FF.Examples.ex11 [variable, in tuple3]

FF.Examples.ex12 [variable, in tuple3]

FF.Examples.ex13 [variable, in tuple3]

FF.Examples.ex14 [variable, in tuple3]

FF.Examples.ex15 [variable, in tuple3]

FF.Examples.ex16 [variable, in tuple3]

FF.Examples.ex17 [variable, in tuple3]

FF.Examples.ex18 [variable, in tuple3]

FF.Examples.ex19 [variable, in tuple3]

FF.Examples.ex2 [variable, in tuple3]

FF.Examples.ex20 [variable, in tuple3]

FF.Examples.ex21 [variable, in tuple3]

FF.Examples.ex3 [variable, in tuple3]

FF.Examples.ex4 [variable, in tuple3]

FF.Examples.ex5 [variable, in tuple3]

FF.Examples.ex6 [variable, in tuple3]

FF.Examples.ex7 [variable, in tuple3]

FF.Examples.ex8 [variable, in tuple3]

FF.Examples.ex9_3 [variable, in tuple3]

FF.Examples.ex9_1 [variable, in tuple3]

FF.Examples.ex9_2 [variable, in tuple3]

FF.FT [variable, in tuple3]

FF.Generic [section, in tuple3]

FF.Generic.cadd [variable, in tuple3]

FF.Generic.cadd_c [variable, in tuple3]

FF.Generic.coef [variable, in tuple3]

FF.Generic.cone [variable, in tuple3]

FF.Generic.conep [variable, in tuple3]

FF.Generic.conep_c [variable, in tuple3]

FF.Generic.cone_c [variable, in tuple3]

FF.Generic.copp [variable, in tuple3]

FF.Generic.copp_c [variable, in tuple3]

FF.Generic.cscale [variable, in tuple3]

FF.Generic.cscale_c [variable, in tuple3]

FF.Generic.czero [variable, in tuple3]

FF.Generic.czerop [variable, in tuple3]

FF.Generic.czerop_c [variable, in tuple3]

FF.Generic.czero_c [variable, in tuple3]

FF.Generic.expr [variable, in tuple3]

FF.Generic.interc [variable, in tuple3]

FF.Generic.interk [variable, in tuple3]

FF.Generic.interv [variable, in tuple3]

FF.Generic.line [variable, in tuple3]

FF.Generic.tvar [variable, in tuple3]

FF.Generic.tvarn [variable, in tuple3]

FF.Generic.tvcompare [variable, in tuple3]

FF.Generic.tvcompare_inj [variable, in tuple3]

FF.Generic.tvcompare_def [variable, in tuple3]

FF.Generic.var [variable, in tuple3]

{c[ _ ]} [notation, in tuple3]

{e1[ _ ]} [notation, in tuple3]

{e[ _ ]} [notation, in tuple3]

{k[ _ ]} [notation, in tuple3]

{l[ _ ]} [notation, in tuple3]

{t[ _ ]} [notation, in tuple3]

{v[ _ ]} [notation, in tuple3]

FF.HP [variable, in tuple3]

FF.K [variable, in tuple3]

FF.NatImplem [section, in tuple3]

FF.NatImplem.interk [variable, in tuple3]

{c[ _ ]} [notation, in tuple3]

{k[ _ ]} [notation, in tuple3]

{m[ _ ]} [notation, in tuple3]

{vs[ _ ]} [notation, in tuple3]

{ _ , _ , _ } [notation, in tuple3]

fget [definition, in Grassmann]

fget_scal [lemma, in Grassmann]

Field [library]

first_deg0 [lemma, in Grassmann]

first_deg0i [lemma, in Grassmann]

fn [definition, in Grassmann]

fn [definition, in Kn]

Fold2 [section, in Aux]

Fold2.A [variable, in Aux]

Fold2.B [variable, in Aux]

Fold2.C [variable, in Aux]

Fold2.f [variable, in Aux]

Fold2.g [variable, in Aux]

fortho [definition, in Grassmann]

forthok [lemma, in Grassmann]

fortho_scal [lemma, in Grassmann]

fortho_refl [lemma, in Grassmann]

fortho_fget [lemma, in Grassmann]

fortho_joinl [lemma, in Grassmann]

fortho_join [lemma, in Grassmann]

fortho_conj [lemma, in Grassmann]

fortho_add [lemma, in Grassmann]

fortho0 [lemma, in Grassmann]

fparams [record, in Field]

fparamsProp [record, in Field]

free [definition, in VectorSpace]

free_nil [lemma, in VectorSpace]

free_cons [lemma, in VectorSpace]

free_incl [lemma, in VectorSpace]

free_perm [lemma, in VectorSpace]

free_elim [definition, in tuple3]

free_elim_c [lemma, in tuple3]

## G

genkE [lemma, in Grassmann]genk_id0 [lemma, in Kn]

genk_inj [lemma, in Kn]

genk0_mprod [lemma, in VectorSpace]

genk0_dec [lemma, in Kn]

gen_inj [lemma, in Kn]

gen_lift [lemma, in Grassmann]

get_homkS [lemma, in Grassmann]

get_hom_ei [lemma, in Grassmann]

get_hom_scal [lemma, in Grassmann]

get_homk0 [lemma, in Grassmann]

get_hom_up [lemma, in Grassmann]

get_hom0 [lemma, in Grassmann]

get_hom_add [lemma, in Grassmann]

get_hom_sum [lemma, in Grassmann]

gprod [definition, in Clifford]

gprodE [lemma, in Clifford]

gprodE_v [lemma, in Clifford]

gprodE_ei [lemma, in Clifford]

gprodkl [lemma, in Clifford]

gprodkr [lemma, in Clifford]

gprod_scalr [lemma, in Clifford]

gprod_assoc [lemma, in Clifford]

gprod_spec1 [lemma, in Clifford]

gprod_e0 [lemma, in Clifford]

gprod_addl [lemma, in Clifford]

gprod_ei [lemma, in Clifford]

gprod_spec2 [lemma, in Clifford]

gprod_all_rev [lemma, in Clifford]

gprod_addr [lemma, in Clifford]

gprod_scall [lemma, in Clifford]

gprod0l [lemma, in Clifford]

gprod0r [lemma, in Clifford]

grade [definition, in Grassmann]

gradeE [lemma, in Grassmann]

grade_meet [lemma, in Grassmann]

grade_join [lemma, in Grassmann]

grade_scal [lemma, in Grassmann]

grade_hom [lemma, in Grassmann]

grade_dual [lemma, in Grassmann]

grade0 [lemma, in Grassmann]

grade0E [lemma, in Grassmann]

grade1_hom [lemma, in Grassmann]

Grassmann [library]

grpod_l0_join [lemma, in Clifford]

gvp [abbreviation, in Clifford]

G3 [library]

## H

has_delta_c [lemma, in tuple3]has_delta [definition, in tuple3]

has_delta_in [lemma, in tuple3]

hom [definition, in G3]

hom [abbreviation, in Clifford]

homd [lemma, in G3]

homE [lemma, in Grassmann]

homk0 [lemma, in Grassmann]

homn_ex [lemma, in Grassmann]

homn_1 [lemma, in Grassmann]

homn_all [lemma, in Grassmann]

hom_first_deg [lemma, in Grassmann]

hom_induct [lemma, in Grassmann]

hom_lt [lemma, in Grassmann]

hom_get_hom [lemma, in Grassmann]

hom0E [lemma, in Grassmann]

hom0K [lemma, in Grassmann]

hom0l [lemma, in G3]

hom0p [lemma, in G3]

hom0r [lemma, in G3]

hom0_E [lemma, in G3]

hom01 [lemma, in G3]

hom1d [lemma, in G3]

hom1E [lemma, in Grassmann]

hom1e [lemma, in Grassmann]

hom1p [lemma, in G3]

hom1_decomposable [lemma, in Grassmann]

hom2 [lemma, in G3]

hom3E [lemma, in G3]

hom3l [lemma, in G3]

hom3r [lemma, in G3]

hom3_1 [lemma, in G3]

## I

ielim [definition, in tuple3]ielim_c [lemma, in tuple3]

injk [lemma, in Grassmann]

inj_e [lemma, in Grassmann]

Inter [constructor, in tuple3]

inter [lemma, in Grassmann]

intera [definition, in tuple3]

interc [definition, in tuple3]

interc_cons [lemma, in tuple3]

interc_nil [lemma, in tuple3]

intere [definition, in tuple3]

intere1 [definition, in tuple3]

intere1_c [lemma, in tuple3]

interl [definition, in tuple3]

interla [definition, in tuple3]

interla_refine [definition, in tuple3]

interm [definition, in tuple3]

intersection [definition, in G3]

intert [definition, in tuple3]

intervs [definition, in tuple3]

intervs_cons [lemma, in tuple3]

intervs_nil [lemma, in tuple3]

inter_elim [definition, in tuple3]

inter_elim_c [lemma, in tuple3]

inter_lines [definition, in G3]

invK [projection, in Field]

invKl [projection, in Field]

invKr [lemma, in Field]

is_vector_space [definition, in Grassmann]

is_decomposable [definition, in Grassmann]

is_vector_space_swap [lemma, in Grassmann]

is_base [definition, in VectorSpace]

is_vector [definition, in Grassmann]

iter [definition, in Aux]

iter_elim_c [lemma, in tuple3]

iter_contra_c [lemma, in tuple3]

iter_free [definition, in tuple3]

iter_split_c [lemma, in tuple3]

iter_contra [definition, in tuple3]

iter_split [definition, in tuple3]

iter_rp [definition, in tuple3]

iter_elim [definition, in tuple3]

iter_step [definition, in tuple3]

iter_free_c [lemma, in tuple3]

iter_step_c [lemma, in tuple3]

## J

join [definition, in Grassmann]joink [lemma, in Grassmann]

joinkl [lemma, in Grassmann]

joinkr [lemma, in Grassmann]

joinl [definition, in Grassmann]

joinlS [lemma, in Grassmann]

joinl_scal [lemma, in Grassmann]

joinl_app [lemma, in Grassmann]

joinl_hom1 [lemma, in Grassmann]

joinl_factor [lemma, in Grassmann]

joinl_addmult [lemma, in Grassmann]

joinl_top [lemma, in Grassmann]

joinl_swap [lemma, in Grassmann]

joinl_join [lemma, in Grassmann]

joinl_all [lemma, in Grassmann]

joinl_base1_perm [lemma, in Grassmann]

joinl0 [lemma, in Grassmann]

joinl0_base1_perm [lemma, in Grassmann]

joinl0_mprod [lemma, in Grassmann]

joinl1 [lemma, in Grassmann]

join_swap [lemma, in G3]

join_e [lemma, in Grassmann]

join_alll [lemma, in Grassmann]

join_assoc [lemma, in Grassmann]

join_scall [lemma, in G3]

join_allhr [lemma, in Grassmann]

join_meet3l [lemma, in G3]

join_meet3r [lemma, in G3]

join_addl [lemma, in G3]

join_allhl [lemma, in Grassmann]

join_ei [lemma, in Grassmann]

join_addl [lemma, in Grassmann]

join_hom_com [lemma, in Grassmann]

join_hom1_id [lemma, in Grassmann]

join_hom_odd [lemma, in Grassmann]

join_addr [lemma, in Grassmann]

join_e0 [lemma, in Grassmann]

join_scalr [lemma, in G3]

join_hom [lemma, in Grassmann]

join_allr [lemma, in Grassmann]

join_scall [lemma, in Grassmann]

join_es [lemma, in Grassmann]

join_addr [lemma, in G3]

join_big [lemma, in Grassmann]

join_scalr [lemma, in Grassmann]

join_meet_swap [lemma, in Grassmann]

join_hom_id [lemma, in Grassmann]

join_meet_distrl [lemma, in Grassmann]

join0 [lemma, in Grassmann]

join0l [lemma, in Grassmann]

join0r [lemma, in Grassmann]

join01E [lemma, in Grassmann]

join1l [lemma, in Grassmann]

join1l [lemma, in G3]

join1r [lemma, in G3]

join1r [lemma, in Grassmann]

join2_meetE [lemma, in Grassmann]

join3_meetE [lemma, in Grassmann]

## K

K [projection, in VectorSpace]K [projection, in Field]

Kadd [definition, in Kn]

Keq [definition, in Kn]

Kgen [definition, in Kn]

Kn [definition, in Kn]

kn [abbreviation, in Clifford]

Kn [definition, in Grassmann]

Kn [section, in Kn]

Kn [library]

kn_induct [lemma, in Kn]

Kn.Hp [variable, in Kn]

Kn.p [variable, in Kn]

_ [.] _ (kn_scope) [notation, in Kn]

'e_ _ (kn_scope) [notation, in Kn]

[ _ ] (kn_scope) [notation, in Kn]

_ [*] _ [notation, in Kn]

K [notation, in Kn]

kn2l [definition, in Kn]

kn2ll2knE [lemma, in Kn]

kn2l_ei [lemma, in Kn]

kn2l_0 [lemma, in Kn]

kn2l_e0 [lemma, in Kn]

kprod [definition, in Kn]

kprodkl [lemma, in Kn]

kprodkr [lemma, in Kn]

kprod_assoc [lemma, in Kn]

kprod_scalr [lemma, in Kn]

kprod_scall [lemma, in Kn]

kprod_addr [lemma, in Kn]

kprod_addl [lemma, in Kn]

kprod0l [lemma, in Kn]

kprod0r [lemma, in Kn]

kprod1l [lemma, in Kn]

kprod1r [lemma, in Kn]

Kproj [definition, in Kn]

Kscal [definition, in Kn]

Ksprod [definition, in Kn]

K0 [definition, in Kn]

K1 [definition, in Clifford]

K1 [definition, in Grassmann]

K2G [definition, in Grassmann]

k2glift [lemma, in Grassmann]

k2g_add [lemma, in Grassmann]

k2g_scal [lemma, in Grassmann]

k2g_hom [lemma, in Grassmann]

k2g_unit [lemma, in Grassmann]

k2g0 [lemma, in Grassmann]

k2l_mprod [lemma, in Kn]

## L

lcompare [definition, in tuple3]lcompare_eq [lemma, in tuple3]

length_split [lemma, in Aux]

lgenk_length [lemma, in VectorSpace]

lift [definition, in Grassmann]

lift [definition, in Kn]

liftk [abbreviation, in Grassmann]

lift_scal [lemma, in Kn]

lift_join [lemma, in Grassmann]

lift_k [lemma, in Grassmann]

lift_e [lemma, in Kn]

lift_contra [lemma, in Grassmann]

lift_cbl [lemma, in Grassmann]

lift_mprod [lemma, in Kn]

lift_add [lemma, in Grassmann]

lift_mcontra [lemma, in Grassmann]

lift_mprod [lemma, in Grassmann]

lift_add [lemma, in Kn]

lift_scal [lemma, in Grassmann]

lift_decomp [lemma, in Grassmann]

lift_joinl [lemma, in Grassmann]

lift_inj [lemma, in Grassmann]

lift0 [lemma, in Kn]

line [definition, in G3]

linsert [definition, in tuple3]

linsert_c [lemma, in tuple3]

linsert_length [lemma, in tuple3]

list_compare [definition, in tuple3]

list_dec [lemma, in Aux]

list_compare_id [lemma, in tuple3]

list_compare_eq [lemma, in tuple3]

list_split [lemma, in Aux]

list_insert [definition, in tuple3]

list_case [lemma, in Aux]

list_app_inj [lemma, in Aux]

lrev [definition, in tuple3]

lrev_c [lemma, in tuple3]

lsort [definition, in tuple3]

lsort_c [lemma, in tuple3]

ltsort [definition, in tuple3]

ltsort_c [lemma, in tuple3]

l_contra_kl [lemma, in Clifford]

l_contra_scall [lemma, in Clifford]

l_contra_addr [lemma, in Clifford]

l_contra_0l [lemma, in Clifford]

l_contra_joinl [lemma, in Clifford]

l_contra_kr [lemma, in Clifford]

l_contra [definition, in Clifford]

l_contra_0r [lemma, in Clifford]

l_contra_conj [lemma, in Clifford]

l_contra_scalr [lemma, in Clifford]

l_contra_ei [lemma, in Clifford]

l_contra_eij [lemma, in Clifford]

l_contra_addl [lemma, in Clifford]

## M

map2_length [lemma, in Aux]mcontra [definition, in Grassmann]

mcontrak [lemma, in Grassmann]

mcontra_one_factor [lemma, in Grassmann]

mcontra_conj [lemma, in Grassmann]

mcontra_add [lemma, in Grassmann]

mcontra_scal [lemma, in Grassmann]

mcontra_id [lemma, in Grassmann]

mcontra_hom [lemma, in Grassmann]

mcontra_hom0 [lemma, in Grassmann]

mcontra_swap [lemma, in Grassmann]

mcontra_app [lemma, in Grassmann]

mcontra_nil [lemma, in Grassmann]

mcontra_cons [lemma, in Grassmann]

mcontra0 [lemma, in Grassmann]

meet [definition, in Grassmann]

meetkl [lemma, in Grassmann]

meetkl0 [lemma, in Grassmann]

meetkr [lemma, in Grassmann]

meetkr0 [lemma, in Grassmann]

meetS [lemma, in Grassmann]

meet_alll [lemma, in Grassmann]

meet_swap [lemma, in G3]

meet_assoc [lemma, in Grassmann]

meet_addr [lemma, in Grassmann]

meet_allr [lemma, in Grassmann]

meet_hom [lemma, in Grassmann]

meet_addl [lemma, in Grassmann]

meet_addr [lemma, in G3]

meet_swapr [lemma, in G3]

meet_join_distrl [lemma, in Grassmann]

meet_scall [lemma, in G3]

meet_scall [lemma, in Grassmann]

meet_hom_com [lemma, in Grassmann]

meet_small [lemma, in Grassmann]

meet_hom_id [lemma, in Grassmann]

meet_addl [lemma, in G3]

meet_join_distrl [lemma, in G3]

meet_scalr [lemma, in G3]

meet_scalr [lemma, in Grassmann]

meet0 [lemma, in Grassmann]

meet0l [lemma, in Grassmann]

meet0r [lemma, in Grassmann]

meet1l [lemma, in Grassmann]

meet1r [lemma, in Grassmann]

minus_minus_le [lemma, in Aux]

minus_match [lemma, in Aux]

minus0_le [lemma, in Aux]

mk_tuplel_c [lemma, in tuple3]

mk_tupler_c [lemma, in tuple3]

mk_tuplel [definition, in tuple3]

mk_tupler [definition, in tuple3]

More [constructor, in tuple3]

mprod [definition, in VectorSpace]

mprod_S [lemma, in VectorSpace]

mprod_2l [lemma, in Grassmann]

mprod_app [lemma, in VectorSpace]

mprod_hom [lemma, in Grassmann]

mprod_cbl [lemma, in VectorSpace]

mprod_perm [lemma, in VectorSpace]

mprod0 [lemma, in VectorSpace]

mprod0l [lemma, in VectorSpace]

mprod0r [lemma, in VectorSpace]

multK [projection, in Field]

multK_com [projection, in Field]

multK_swap [lemma, in Field]

multK_assoc [projection, in Field]

multK_cancel [lemma, in Field]

multK_integral [lemma, in Field]

multK_m1_m1 [lemma, in Field]

multK0l [lemma, in Field]

multK0r [lemma, in Field]

multK1l [projection, in Field]

multK1r [lemma, in Field]

## N

natc [definition, in tuple3]natc_id [lemma, in tuple3]

natc_correct [lemma, in tuple3]

natc_eq [lemma, in tuple3]

ndo_auto [definition, in tuple3]

ndo_auto_c [definition, in tuple3]

nfelim [definition, in tuple3]

nfelim_c [lemma, in tuple3]

nielim [definition, in tuple3]

nielim_c [lemma, in tuple3]

n_to_K [definition, in Field]

n_to_K_minus [lemma, in Field]

n_to_K1 [lemma, in Field]

n_to_K_mult [lemma, in Field]

n_to_K_add [lemma, in Field]

n_to_K0 [lemma, in Field]

## O

one_diff_zero [projection, in Field]one_factor [definition, in Grassmann]

one_factor_zero [lemma, in Grassmann]

one_factor_hom [lemma, in Grassmann]

one_factor0 [lemma, in Grassmann]

online [definition, in G3]

online_def [lemma, in G3]

online1 [definition, in G3]

oppK [projection, in Field]

oppk [lemma, in Grassmann]

oppKl [lemma, in Field]

oppKr [projection, in Field]

oppK0 [lemma, in Field]

opp_multK1l [lemma, in Field]

opp_oppK [lemma, in Field]

opp_multKl [lemma, in Field]

opp_multKr [lemma, in Field]

opp_addK [lemma, in Field]

opp_multK1r [lemma, in Field]

## P

Pappus [lemma, in G3]params [record, in VectorSpace]

ParamsProp [section, in Field]

ParamsProp.Hp [variable, in Field]

ParamsProp.p [variable, in Field]

_ ^ _ (field_scope) [notation, in Field]

Perm [section, in Aux]

perm [inductive, in Aux]

perm_trans [constructor, in Aux]

perm_sym [lemma, in Aux]

perm_skip [constructor, in Aux]

perm_incl_inv [lemma, in Aux]

perm_length [lemma, in Aux]

perm_in_inv [lemma, in Aux]

perm_incl_l [lemma, in Aux]

perm_id [constructor, in Aux]

perm_cons_app [lemma, in Aux]

perm_incl_r [lemma, in Aux]

perm_swap [constructor, in Aux]

perm_in [lemma, in Aux]

Perm.A [variable, in Aux]

point [definition, in G3]

Pp [definition, in G3]

Pp [definition, in tuple3]

prodk [definition, in Clifford]

prod_scal_scalr [lemma, in Clifford]

prod_scal0r [lemma, in Clifford]

prod_scal_addr [lemma, in Clifford]

prod_scal0l [lemma, in Clifford]

prod_scal_addl [lemma, in Clifford]

prod_scal [definition, in Clifford]

prod_scal_sym [lemma, in Clifford]

prod_scal_scall [lemma, in Clifford]

proj [definition, in Grassmann]

proj [definition, in Kn]

projk [abbreviation, in Clifford]

projk [abbreviation, in Grassmann]

projn [lemma, in Grassmann]

proj_lt [lemma, in Grassmann]

proj_hom0_eq [lemma, in Grassmann]

proj_homk [lemma, in Grassmann]

proj_add [lemma, in Kn]

proj_scal [lemma, in Kn]

proj_base_length [lemma, in Grassmann]

proj_e [lemma, in Kn]

proj_homn_eq [lemma, in Grassmann]

proj0 [lemma, in Kn]

proj0 [lemma, in Grassmann]

pscal [definition, in Kn]

pscal_com [lemma, in Kn]

pscal_addl [lemma, in Kn]

pscal_e [lemma, in Kn]

pscal_meet [lemma, in Grassmann]

pscal_addr [lemma, in Kn]

pscal_scall [lemma, in Kn]

pscal_scalr [lemma, in Kn]

pscal_join [lemma, in Grassmann]

pscal0l [lemma, in Kn]

pscal0r [lemma, in Kn]

pseudo_invE [lemma, in Clifford]

pseudo_inv [definition, in Clifford]

p2v [definition, in G3]

## Q

Qparams [definition, in Grassmann]## R

RBfalse [constructor, in tuple3]RBtrue [constructor, in tuple3]

reorder [definition, in tuple3]

reorder_c [lemma, in tuple3]

resolve [definition, in tuple3]

resolve_c [lemma, in tuple3]

rev [definition, in tuple3]

rev [definition, in Clifford]

revk [lemma, in Clifford]

rev_join [lemma, in Clifford]

rev_add [lemma, in Clifford]

rev_hom [lemma, in Clifford]

rev_invo [lemma, in Clifford]

rev_scal [lemma, in Clifford]

rev_conj [lemma, in Clifford]

rev0 [lemma, in Clifford]

rp [inductive, in tuple3]

rp_val [definition, in tuple3]

## S

scalE [projection, in VectorSpace]scalE_mprod [lemma, in VectorSpace]

scalE_swap [lemma, in VectorSpace]

scalE_add0 [lemma, in VectorSpace]

scalE_opp [lemma, in VectorSpace]

scalE_integral [lemma, in VectorSpace]

scalE0l [projection, in VectorSpace]

scalE0r [lemma, in VectorSpace]

scalE1 [projection, in VectorSpace]

scalk [lemma, in Grassmann]

scal_addE0 [lemma, in VectorSpace]

scal_multE [projection, in VectorSpace]

scal_integral [lemma, in Kn]

scal_hom [lemma, in Grassmann]

scal_integral [lemma, in Grassmann]

scal_addEl [projection, in VectorSpace]

scal_addEr [projection, in VectorSpace]

scmp [definition, in tuple3]

scmp_c [lemma, in tuple3]

SFree [constructor, in tuple3]

sign [inductive, in tuple3]

smult [definition, in tuple3]

smult3 [definition, in tuple3]

Sm1 [constructor, in tuple3]

sopp [definition, in tuple3]

splitll [lemma, in Grassmann]

splitlr [lemma, in Grassmann]

splitrl [lemma, in Grassmann]

splitrr [lemma, in Grassmann]

splitrr [lemma, in G3]

split_meetl [lemma, in G3]

split_meetr [lemma, in G3]

split3b [lemma, in G3]

split3b_v2 [lemma, in G3]

split3b_v1 [lemma, in G3]

split3l [lemma, in G3]

sprod [inductive, in tuple3]

SProd [constructor, in tuple3]

sProp [projection, in VectorSpace]

step [definition, in tuple3]

step_c [lemma, in tuple3]

Stop [constructor, in tuple3]

stype [projection, in VectorSpace]

sub_add [lemma, in G3]

sub_add [lemma, in Grassmann]

sub0l [lemma, in Grassmann]

sub0r [lemma, in Grassmann]

sumEl [lemma, in Grassmann]

sumEr [lemma, in Grassmann]

sum_ext [lemma, in Grassmann]

S0 [constructor, in tuple3]

S1 [constructor, in tuple3]

s2k [definition, in tuple3]

s2km [lemma, in tuple3]

s2ko [lemma, in tuple3]

## T

TBool [inductive, in tuple3]tcompare [definition, in tuple3]

tcompare_eq [lemma, in tuple3]

term [definition, in tuple3]

term_opp [definition, in tuple3]

term_cmp [definition, in tuple3]

term_zerop [definition, in tuple3]

term_add_c [lemma, in tuple3]

term_zerop_c [lemma, in tuple3]

term_scale [definition, in tuple3]

term_add [definition, in tuple3]

term_opp_c [lemma, in tuple3]

term_scale_c [lemma, in tuple3]

tin [definition, in tuple3]

tin_correct [lemma, in tuple3]

Trans [section, in VectorSpace]

Trans.f [variable, in VectorSpace]

Trans.g [variable, in VectorSpace]

Trans.g1 [variable, in VectorSpace]

Trans.Hf0 [variable, in VectorSpace]

Trans.Hf1 [variable, in VectorSpace]

Trans.Hf2 [variable, in VectorSpace]

Trans.Hg [variable, in VectorSpace]

Trans.Hp [variable, in VectorSpace]

Trans.Hp1 [variable, in VectorSpace]

Trans.p [variable, in VectorSpace]

Trans.p1 [variable, in VectorSpace]

tsort [definition, in tuple3]

tsort_c [lemma, in tuple3]

tsplit [definition, in tuple3]

tsplit_c [lemma, in tuple3]

tsplit3 [definition, in tuple3]

tsplit3_c [lemma, in tuple3]

tsubst [definition, in tuple3]

tsubst_c [lemma, in tuple3]

tuple [inductive, in tuple3]

Tuple [constructor, in tuple3]

tuple3 [library]

tvar [definition, in tuple3]

tvarn [definition, in tuple3]

tvcompare [definition, in tuple3]

tvcompare_eq [lemma, in tuple3]

tvcompare_refl [lemma, in tuple3]

tvcompare_inj [lemma, in tuple3]

tvcompare_def [lemma, in tuple3]

## U

uniq [inductive, in Aux]Uniq [section, in Aux]

uniq_app_inv_l [lemma, in Aux]

uniq_app_inv_r [lemma, in Aux]

uniq_nil [constructor, in Aux]

uniq_free [lemma, in VectorSpace]

uniq_cons_inv [lemma, in Aux]

uniq_cons [constructor, in Aux]

uniq_perm [lemma, in Aux]

Uniq.A [variable, in Aux]

## V

Vadd [definition, in Grassmann]Vadd [definition, in G3]

var [definition, in tuple3]

Vconj [definition, in Grassmann]

Vcontra [definition, in Grassmann]

Vdecompose [definition, in Grassmann]

Vdual [definition, in Grassmann]

Vdual [definition, in G3]

Vect [section, in Grassmann]

vect [abbreviation, in Clifford]

vect [definition, in G3]

Vect [section, in G3]

Vect [definition, in Grassmann]

Vect [section, in Clifford]

VectorSpace [section, in VectorSpace]

VectorSpace [library]

VectorSpace.Hp [variable, in VectorSpace]

VectorSpace.p [variable, in VectorSpace]

VectorSpace.sfP [variable, in VectorSpace]

_ *X* _ (vector_scope) [notation, in VectorSpace]

vect_hom_induct [lemma, in Grassmann]

vect_induct [lemma, in Grassmann]

Vect.add_com [variable, in G3]

Vect.add_assoc [variable, in G3]

Vect.add0l [variable, in G3]

Vect.add0r [variable, in G3]

Vect.F [variable, in G3]

Vect.FT [variable, in G3]

Vect.Hp [variable, in Clifford]

Vect.HP [variable, in G3]

Vect.Hp [variable, in Grassmann]

Vect.join_assoc [variable, in G3]

Vect.join_id [variable, in G3]

Vect.join0l [variable, in G3]

Vect.join0r [variable, in G3]

Vect.meet_assoc [variable, in G3]

Vect.meet_alll [variable, in G3]

Vect.meet_allr [variable, in G3]

Vect.p [variable, in Grassmann]

Vect.p [variable, in Clifford]

Vect.scal_addr [variable, in G3]

Vect.scal_addl [variable, in G3]

Vect.scal_integral [variable, in G3]

Vect.scal_mult [variable, in G3]

Vect.scal_mul [variable, in G3]

Vect.scal0l [variable, in G3]

Vect.scal0r [variable, in G3]

Vect.scal1l [variable, in G3]

_ ?= 0 (g_scope) [notation, in Grassmann]

K (g_scope) [notation, in Clifford]

1 (g_scope) [notation, in Grassmann]

[ _ ] (g_scope) [notation, in Grassmann]

K (g_scope) [notation, in Grassmann]

_ ^'dl (g_scope) [notation, in Grassmann]

_ ^'l (g_scope) [notation, in Grassmann]

'e_ _ (g_scope) [notation, in Grassmann]

_ - _ (g_scope) [notation, in Grassmann]

_ .* _ (Kn_scope) [notation, in Clifford]

_ ∨ _ (type_scope) [notation, in Grassmann]

_ .* _ [notation, in Clifford]

_ ^d_ _ [notation, in Grassmann]

_ ∧ _ [notation, in G3]

_ ^_'f [notation, in Grassmann]

_ + _ [notation, in Clifford]

_ ?= _ [notation, in G3]

_ ^_'t [notation, in Grassmann]

_ [* _ ] _ [notation, in Clifford]

_ ^_'f [notation, in Clifford]

_ [. _ ] _ [notation, in Clifford]

_ ^d_'f [notation, in Grassmann]

_ + _ [notation, in G3]

_ ∧ _ [notation, in Grassmann]

_ 'L[ _ ] _ [notation, in Clifford]

_ ^_ _ [notation, in Grassmann]

_ - _ [notation, in G3]

_ ∨ _ [notation, in G3]

_ ^d_'t [notation, in Grassmann]

_ ∧ _ [notation, in Clifford]

_ .* _ [notation, in G3]

E [notation, in G3]

E [notation, in G3]

E [notation, in Grassmann]

kn [notation, in Grassmann]

#< _ , _ ># [notation, in Grassmann]

#< _ , _ ># [notation, in Clifford]

#<< _ , _ >># [notation, in Grassmann]

'C[ _ ] [notation, in G3]

'C[ _ ] [notation, in Grassmann]

'C[ _ ] [notation, in Clifford]

'dC[ _ ] [notation, in G3]

'dC[ _ ] [notation, in Grassmann]

'e_ _ [notation, in Clifford]

'kn _ [notation, in Grassmann]

'Pi[ _ ] [notation, in Clifford]

'P[ _ ] [notation, in Clifford]

'R[ _ ] [notation, in Clifford]

'v_ _ [notation, in Clifford]

'v_ _ [notation, in Grassmann]

'@ _ [notation, in Clifford]

'@ _ [notation, in Grassmann]

'@ _ [notation, in G3]

'[ _ , _ , _ ] [notation, in G3]

0 [notation, in G3]

1 [notation, in G3]

[ _ ] [notation, in Clifford]

Veq [definition, in G3]

Veq [definition, in Grassmann]

Vgen [definition, in Grassmann]

Vgenk [definition, in Grassmann]

Vgenk [definition, in G3]

Vjoin [definition, in Grassmann]

Vjoin [definition, in G3]

Vmeet [definition, in Grassmann]

Vmeet [definition, in G3]

vn_eparams [definition, in Kn]

vn_eparams [definition, in Clifford]

vn_eparams [definition, in Grassmann]

vparamsProp [record, in VectorSpace]

Vscal [definition, in G3]

Vscal [definition, in Grassmann]

Vsub [definition, in G3]

v_eparams [definition, in Kn]

v_eparams [definition, in Grassmann]

v0 [projection, in Field]

V0 [definition, in Grassmann]

v1 [projection, in Field]

V1 [definition, in Grassmann]

v2k [definition, in Grassmann]

v2l_length [lemma, in Grassmann]

## Z

Z_to_K_opp [lemma, in Field]Z_to_K_minus [lemma, in Field]

Z_to_K [definition, in Field]

Z_to_K_mult [lemma, in Field]

Z_to_K_pos [lemma, in Field]

Z_to_K_add [lemma, in Field]

## other

0 (field_scope) [notation, in Field]_ + _ (field_scope) [notation, in Field]

1 (field_scope) [notation, in Field]

_ ^-1 (field_scope) [notation, in Field]

_ ^ _ (field_scope) [notation, in Field]

_ * _ (field_scope) [notation, in Field]

_ ?= _ (field_scope) [notation, in Field]

- _ (field_scope) [notation, in Field]

[ _ ] (Gn_scope) [notation, in Grassmann]

'e_ _ (Gn_scope) [notation, in Grassmann]

_ [*] _ (Kn_scope) [notation, in Kn]

_ [.] _ (Kn_scope) [notation, in Kn]

[ _ ] (Kn_scope) [notation, in Kn]

'e_ _ (Kn_scope) [notation, in Kn]

_ ?= _ (nat_scope) [notation, in Aux]

_ .+2 (nat_scope) [notation, in Aux]

_ .+1 (nat_scope) [notation, in Aux]

_ .* _ (vector_scope) [notation, in VectorSpace]

0 (vector_scope) [notation, in VectorSpace]

_ ?= _ (vector_scope) [notation, in VectorSpace]

_ + _ (vector_scope) [notation, in VectorSpace]

_ *X* _ (vector_scope) [notation, in VectorSpace]

_ ∨ _ [notation, in G3]

_ is_the_intersection_of [ _ , _ ] and [ _ , _ ] [notation, in G3]

_ .* _ [notation, in G3]

_ + _ [notation, in G3]

_ ?= _ [notation, in G3]

_ - _ [notation, in G3]

_ ∧ _ [notation, in G3]

_ :=: xfree on [ _ , _ ] ( _ , _ ) [notation, in G3]

_ is_free_on [ _ , _ ] [notation, in G3]

E [notation, in G3]

'C[ _ ] [notation, in G3]

'dC[ _ ] [notation, in G3]

'@ _ [notation, in G3]

'[ _ , _ , _ ] [notation, in G3]

0 [notation, in G3]

1 [notation, in G3]

[ _ , _ , _ ] are_collinear [notation, in G3]

# Projection Index

## A

addE [in VectorSpace]addE_com [in VectorSpace]

addE_assoc [in VectorSpace]

addE0l [in VectorSpace]

addK [in Field]

addK_assoc [in Field]

addK_com [in Field]

addK0l [in Field]

add_multKl [in Field]

## D

dim [in VectorSpace]## E

E [in VectorSpace]eqE [in VectorSpace]

eqE_dec [in VectorSpace]

eqK [in Field]

eqK_dec [in Field]

E0 [in VectorSpace]

## I

invK [in Field]invKl [in Field]

## K

K [in VectorSpace]K [in Field]

## M

multK [in Field]multK_com [in Field]

multK_assoc [in Field]

multK1l [in Field]

## O

one_diff_zero [in Field]oppK [in Field]

oppKr [in Field]

## S

scalE [in VectorSpace]scalE0l [in VectorSpace]

scalE1 [in VectorSpace]

scal_multE [in VectorSpace]

scal_addEl [in VectorSpace]

scal_addEr [in VectorSpace]

sProp [in VectorSpace]

stype [in VectorSpace]

## V

v0 [in Field]v1 [in Field]

# Record Index

## E

eparams [in VectorSpace]## F

fparams [in Field]fparamsProp [in Field]

## P

params [in VectorSpace]## V

vparamsProp [in VectorSpace]# Lemma Index

## A

addE_cancell [in VectorSpace]addE_mprod [in VectorSpace]

addE_eq_opp [in VectorSpace]

addE_swap [in VectorSpace]

addE_cancelr [in VectorSpace]

addE0r [in VectorSpace]

addk [in Grassmann]

addK_cancel [in Field]

addK_eq_opp [in Field]

addK0r [in Field]

add_multKr [in Field]

add_hom [in Grassmann]

all_prods_lift [in Grassmann]

all_prods_free [in Grassmann]

all_prods_cons [in Grassmann]

all_hom1_cor [in Grassmann]

all_hom [in Grassmann]

all_prods_length [in Grassmann]

all_prods_id [in Grassmann]

all_prods1 [in Grassmann]

all_prods_hom [in Grassmann]

all_prods_nil [in Grassmann]

andbP [in Aux]

## B

base_nil [in Grassmann]base_lift [in Grassmann]

base_free [in Grassmann]

base_in [in Grassmann]

base_length [in Kn]

base_length [in Grassmann]

base_n [in Grassmann]

base_hom [in Grassmann]

base_lt_nil [in Grassmann]

base_free [in Kn]

base0 [in Grassmann]

base1_length [in Grassmann]

base1_S [in Grassmann]

bin_def [in Aux]

bin_more [in Aux]

bin_0 [in Aux]

bin_nn [in Aux]

bin_1 [in Aux]

bracket_defE [in G3]

bracket_defr [in G3]

bracket_norm [in G3]

bracket_free [in G3]

bracket_swapl [in G3]

bracket_swapr [in G3]

bracket_defl [in G3]

bracket_expand [in G3]

bracket0l [in G3]

bracket0m [in G3]

bracket0r [in G3]

bracket0_collinear [in G3]

b2PropT [in Aux]

## C

cadd_opp [in tuple3]cadd_c [in tuple3]

cblk_homk_equiv [in Grassmann]

cblnil [in VectorSpace]

cbl_incl [in VectorSpace]

cbl_joinl0_mprod [in Grassmann]

cbl_join_com [in Grassmann]

cbl_all_prods [in Grassmann]

cbl_hom [in Grassmann]

cbl_joinl0 [in Grassmann]

cbl_base1_list_split [in Grassmann]

cbl_map_inv [in VectorSpace]

cbl_base_join_com [in Grassmann]

cbl_contra [in Grassmann]

cbl_mprod [in VectorSpace]

cbl_base [in Kn]

cbl_mcontra [in Grassmann]

cbl_base1_split [in Grassmann]

cbl_map [in VectorSpace]

cbl_trans [in VectorSpace]

cbl_cons [in Grassmann]

cbl_join_id [in Grassmann]

cbl_base_join_id [in Grassmann]

cbl_joinl [in Grassmann]

cbl0_inv [in VectorSpace]

cbl1 [in VectorSpace]

cbl1_hom1_equiv [in Grassmann]

ccons_c [in tuple3]

cdual_cliff [in Clifford]

collinear_bracket [in G3]

collinear_bracket0 [in G3]

conep_c [in tuple3]

conjf_meetl [in Grassmann]

conjf_hom [in Grassmann]

conjf_prod_scal [in Clifford]

conjf_meetr [in Grassmann]

conjf_gprod [in Clifford]

conjf_join [in Grassmann]

conjk [in Grassmann]

conjt [in Grassmann]

conjt_hom [in Grassmann]

conj_scal [in Grassmann]

conj_swap [in Grassmann]

conj_add [in Grassmann]

conj_dual [in Grassmann]

conj_hom [in Grassmann]

conj_all [in Grassmann]

conj_neg [in Grassmann]

conj_const [in Grassmann]

conj_dconst [in Grassmann]

conj_e [in Grassmann]

conj_invo [in Grassmann]

conj0 [in Grassmann]

constk [in Grassmann]

const_scal [in Grassmann]

const_add [in Grassmann]

const_hom [in Grassmann]

const_dual [in Grassmann]

const_join [in Grassmann]

const0 [in Grassmann]

const1 [in G3]

contraction_v3 [in G3]

contraction_v2 [in G3]

contraction_rule_c [in tuple3]

contraction_v1 [in G3]

contraction_v0 [in G3]

contraE [in Grassmann]

contrak [in Grassmann]

contra_join [in Grassmann]

contra_scall [in Grassmann]

contra_const [in Grassmann]

contra_id [in Grassmann]

contra_hom0 [in Grassmann]

contra_swap [in Grassmann]

contra_e [in Grassmann]

contra_addl [in Grassmann]

contra_conj [in Grassmann]

contra_addr [in Grassmann]

contra_scalr [in Grassmann]

contra_hom [in Grassmann]

contra0l [in Grassmann]

contra0r [in Grassmann]

copp_c [in tuple3]

cscale_c [in tuple3]

czerop_opp [in tuple3]

czerop_c [in tuple3]

c0_c [in tuple3]

c1_c [in tuple3]

## D

dconjf_meetd [in Grassmann]dconjf_joinr [in Grassmann]

dconjf_hom [in Grassmann]

dconjf_meet [in Grassmann]

dconjf_joinl [in Grassmann]

dconjk [in Grassmann]

dconjt [in Grassmann]

dconjt_hom [in Grassmann]

dconj_const [in Grassmann]

dconj_dual [in Grassmann]

dconj_all [in Grassmann]

dconj_scal [in Grassmann]

dconj_conj_swap [in Grassmann]

dconj_conj [in Grassmann]

dconj_swap [in Grassmann]

dconj_neg [in Grassmann]

dconj_dconst [in Grassmann]

dconj_hom [in Grassmann]

dconj_add [in Grassmann]

dconj_invo [in Grassmann]

dconj0 [in Grassmann]

dconst_dual [in Grassmann]

dconst_meet [in Grassmann]

dconst_scal [in Grassmann]

dconst_all [in Grassmann]

dconst_add [in Grassmann]

dconst_hom [in Grassmann]

dconst0 [in Grassmann]

deck0 [in Grassmann]

decomposable_factor [in Grassmann]

decomposekSS [in Grassmann]

decomposek_cor [in Grassmann]

decompose_cor [in Grassmann]

decomp_hom [in Grassmann]

decomp_one_factor0 [in Grassmann]

decomp_cbl [in Grassmann]

decomp_one_factor_hom [in Grassmann]

decomp_one_factor_join [in Grassmann]

delta_c [in tuple3]

Desargues [in G3]

div2_prop [in Aux]

div2_double_p [in Aux]

dlift_mprod [in Grassmann]

dlift_scal [in Grassmann]

dlift_add [in Grassmann]

dmap2_eql [in Kn]

do_auto_c [in tuple3]

do_elim_c [in tuple3]

do_contra_c [in tuple3]

do_free_c [in tuple3]

dualE [in Clifford]

dualk [in Grassmann]

dual_hom [in Grassmann]

dual_base [in Grassmann]

dual_invoE [in Grassmann]

dual_invoE [in G3]

dual_invo [in Grassmann]

dual_meet [in Grassmann]

dual_add [in Grassmann]

dual_join [in Grassmann]

dual_scal [in Grassmann]

dual_join_compl [in Grassmann]

dual_all [in Grassmann]

dual0 [in Grassmann]

dual0E [in Grassmann]

dual1 [in Grassmann]

## E

edelta_c [in tuple3]edelta_in [in tuple3]

einsert_length [in tuple3]

einsert_c [in tuple3]

einsert0_c [in tuple3]

en_def [in Grassmann]

eqE_spec [in VectorSpace]

eqE_refl [in VectorSpace]

eqKI [in Field]

eqK_spec [in Field]

eql_sym [in Kn]

eql_refl [in Kn]

eql_trans [in Kn]

eq_natP [in Aux]

eq0I [in Grassmann]

eq0_dec [in Grassmann]

eq0_spec [in Grassmann]

eremove_c [in tuple3]

etsort_c [in tuple3]

expand_meetr [in G3]

expand_meetl [in G3]

expKm1_2E [in Field]

expKm1_sub [in Field]

expKm1_odd [in Field]

expKm1_n0 [in Field]

expKm1_2 [in Field]

expKm1_even [in Field]

expKS [in Field]

expK_add [in Field]

expK_integral [in Field]

expK2m1 [in Field]

expS [in Aux]

exp0 [in Aux]

ex1_proof [in tuple3]

ex10_proof1 [in tuple3]

ex10_proof2 [in tuple3]

ex11_proof [in tuple3]

ex12_proof [in tuple3]

ex13_proof [in tuple3]

ex14_proof [in tuple3]

ex15_proof [in tuple3]

ex16_proof [in tuple3]

ex17_proof [in tuple3]

ex18_proof [in tuple3]

ex19_proof [in tuple3]

ex2_proof [in tuple3]

ex20_proof [in tuple3]

ex3_proof [in tuple3]

ex4_proof [in tuple3]

ex5_l [in tuple3]

ex6_proof [in tuple3]

ex8_proof [in tuple3]

ex9_proof3 [in tuple3]

ex9_proof1 [in tuple3]

ex9_proof2 [in tuple3]

e_in_base [in Kn]

e_in_base_ex [in Kn]

e_in_base1_ex [in Grassmann]

e_in_base1 [in Grassmann]

## F

factork [in Grassmann]factor_hom [in Grassmann]

factor_scal [in Grassmann]

factor_add [in Grassmann]

factor_ortho [in Grassmann]

factor_factor [in Grassmann]

factor_hom0E [in Grassmann]

factor_id [in Grassmann]

factor0 [in Grassmann]

factor0_hom0 [in Grassmann]

fbracket_norm [in G3]

felim_c [in tuple3]

fget_scal [in Grassmann]

first_deg0 [in Grassmann]

first_deg0i [in Grassmann]

forthok [in Grassmann]

fortho_scal [in Grassmann]

fortho_refl [in Grassmann]

fortho_fget [in Grassmann]

fortho_joinl [in Grassmann]

fortho_join [in Grassmann]

fortho_conj [in Grassmann]

fortho_add [in Grassmann]

fortho0 [in Grassmann]

free_nil [in VectorSpace]

free_cons [in VectorSpace]

free_incl [in VectorSpace]

free_perm [in VectorSpace]

free_elim_c [in tuple3]

## G

genkE [in Grassmann]genk_id0 [in Kn]

genk_inj [in Kn]

genk0_mprod [in VectorSpace]

genk0_dec [in Kn]

gen_inj [in Kn]

gen_lift [in Grassmann]

get_homkS [in Grassmann]

get_hom_ei [in Grassmann]

get_hom_scal [in Grassmann]

get_homk0 [in Grassmann]

get_hom_up [in Grassmann]

get_hom0 [in Grassmann]

get_hom_add [in Grassmann]

get_hom_sum [in Grassmann]

gprodE [in Clifford]

gprodE_v [in Clifford]

gprodE_ei [in Clifford]

gprodkl [in Clifford]

gprodkr [in Clifford]

gprod_scalr [in Clifford]

gprod_assoc [in Clifford]

gprod_spec1 [in Clifford]

gprod_e0 [in Clifford]

gprod_addl [in Clifford]

gprod_ei [in Clifford]

gprod_spec2 [in Clifford]

gprod_all_rev [in Clifford]

gprod_addr [in Clifford]

gprod_scall [in Clifford]

gprod0l [in Clifford]

gprod0r [in Clifford]

gradeE [in Grassmann]

grade_meet [in Grassmann]

grade_join [in Grassmann]

grade_scal [in Grassmann]

grade_hom [in Grassmann]

grade_dual [in Grassmann]

grade0 [in Grassmann]

grade0E [in Grassmann]

grade1_hom [in Grassmann]

grpod_l0_join [in Clifford]

## H

has_delta_c [in tuple3]has_delta_in [in tuple3]

homd [in G3]

homE [in Grassmann]

homk0 [in Grassmann]

homn_ex [in Grassmann]

homn_1 [in Grassmann]

homn_all [in Grassmann]

hom_first_deg [in Grassmann]

hom_induct [in Grassmann]

hom_lt [in Grassmann]

hom_get_hom [in Grassmann]

hom0E [in Grassmann]

hom0K [in Grassmann]

hom0l [in G3]

hom0p [in G3]

hom0r [in G3]

hom0_E [in G3]

hom01 [in G3]

hom1d [in G3]

hom1E [in Grassmann]

hom1e [in Grassmann]

hom1p [in G3]

hom1_decomposable [in Grassmann]

hom2 [in G3]

hom3E [in G3]

hom3l [in G3]

hom3r [in G3]

hom3_1 [in G3]

## I

ielim_c [in tuple3]injk [in Grassmann]

inj_e [in Grassmann]

inter [in Grassmann]

interc_cons [in tuple3]

interc_nil [in tuple3]

intere1_c [in tuple3]

intervs_cons [in tuple3]

intervs_nil [in tuple3]

inter_elim_c [in tuple3]

invKr [in Field]

is_vector_space_swap [in Grassmann]

iter_elim_c [in tuple3]

iter_contra_c [in tuple3]

iter_split_c [in tuple3]

iter_free_c [in tuple3]

iter_step_c [in tuple3]

## J

joink [in Grassmann]joinkl [in Grassmann]

joinkr [in Grassmann]

joinlS [in Grassmann]

joinl_scal [in Grassmann]

joinl_app [in Grassmann]

joinl_hom1 [in Grassmann]

joinl_factor [in Grassmann]

joinl_addmult [in Grassmann]

joinl_top [in Grassmann]

joinl_swap [in Grassmann]

joinl_join [in Grassmann]

joinl_all [in Grassmann]

joinl_base1_perm [in Grassmann]

joinl0 [in Grassmann]

joinl0_base1_perm [in Grassmann]

joinl0_mprod [in Grassmann]

joinl1 [in Grassmann]

join_swap [in G3]

join_e [in Grassmann]

join_alll [in Grassmann]

join_assoc [in Grassmann]

join_scall [in G3]

join_allhr [in Grassmann]

join_meet3l [in G3]

join_meet3r [in G3]

join_addl [in G3]

join_allhl [in Grassmann]

join_ei [in Grassmann]

join_addl [in Grassmann]

join_hom_com [in Grassmann]

join_hom1_id [in Grassmann]

join_hom_odd [in Grassmann]

join_addr [in Grassmann]

join_e0 [in Grassmann]

join_scalr [in G3]

join_hom [in Grassmann]

join_allr [in Grassmann]

join_scall [in Grassmann]

join_es [in Grassmann]

join_addr [in G3]

join_big [in Grassmann]

join_scalr [in Grassmann]

join_meet_swap [in Grassmann]

join_hom_id [in Grassmann]

join_meet_distrl [in Grassmann]

join0 [in Grassmann]

join0l [in Grassmann]

join0r [in Grassmann]

join01E [in Grassmann]

join1l [in Grassmann]

join1l [in G3]

join1r [in G3]

join1r [in Grassmann]

join2_meetE [in Grassmann]

join3_meetE [in Grassmann]

## K

kn_induct [in Kn]kn2ll2knE [in Kn]

kn2l_ei [in Kn]

kn2l_0 [in Kn]

kn2l_e0 [in Kn]

kprodkl [in Kn]

kprodkr [in Kn]

kprod_assoc [in Kn]

kprod_scalr [in Kn]

kprod_scall [in Kn]

kprod_addr [in Kn]

kprod_addl [in Kn]

kprod0l [in Kn]

kprod0r [in Kn]

kprod1l [in Kn]

kprod1r [in Kn]

k2glift [in Grassmann]

k2g_add [in Grassmann]

k2g_scal [in Grassmann]

k2g_hom [in Grassmann]

k2g_unit [in Grassmann]

k2g0 [in Grassmann]

k2l_mprod [in Kn]

## L

lcompare_eq [in tuple3]length_split [in Aux]

lgenk_length [in VectorSpace]

lift_scal [in Kn]

lift_join [in Grassmann]

lift_k [in Grassmann]

lift_e [in Kn]

lift_contra [in Grassmann]

lift_cbl [in Grassmann]

lift_mprod [in Kn]

lift_add [in Grassmann]

lift_mcontra [in Grassmann]

lift_mprod [in Grassmann]

lift_add [in Kn]

lift_scal [in Grassmann]

lift_decomp [in Grassmann]

lift_joinl [in Grassmann]

lift_inj [in Grassmann]

lift0 [in Kn]

linsert_c [in tuple3]

linsert_length [in tuple3]

list_dec [in Aux]

list_compare_id [in tuple3]

list_compare_eq [in tuple3]

list_split [in Aux]

list_case [in Aux]

list_app_inj [in Aux]

lrev_c [in tuple3]

lsort_c [in tuple3]

ltsort_c [in tuple3]

l_contra_kl [in Clifford]

l_contra_scall [in Clifford]

l_contra_addr [in Clifford]

l_contra_0l [in Clifford]

l_contra_joinl [in Clifford]

l_contra_kr [in Clifford]

l_contra_0r [in Clifford]

l_contra_conj [in Clifford]

l_contra_scalr [in Clifford]

l_contra_ei [in Clifford]

l_contra_eij [in Clifford]

l_contra_addl [in Clifford]

## M

map2_length [in Aux]mcontrak [in Grassmann]

mcontra_one_factor [in Grassmann]

mcontra_conj [in Grassmann]

mcontra_add [in Grassmann]

mcontra_scal [in Grassmann]

mcontra_id [in Grassmann]

mcontra_hom [in Grassmann]

mcontra_hom0 [in Grassmann]

mcontra_swap [in Grassmann]

mcontra_app [in Grassmann]

mcontra_nil [in Grassmann]

mcontra_cons [in Grassmann]

mcontra0 [in Grassmann]

meetkl [in Grassmann]

meetkl0 [in Grassmann]

meetkr [in Grassmann]

meetkr0 [in Grassmann]

meetS [in Grassmann]

meet_alll [in Grassmann]

meet_swap [in G3]

meet_assoc [in Grassmann]

meet_addr [in Grassmann]

meet_allr [in Grassmann]

meet_hom [in Grassmann]

meet_addl [in Grassmann]

meet_addr [in G3]

meet_swapr [in G3]

meet_join_distrl [in Grassmann]

meet_scall [in G3]

meet_scall [in Grassmann]

meet_hom_com [in Grassmann]

meet_small [in Grassmann]

meet_hom_id [in Grassmann]

meet_addl [in G3]

meet_join_distrl [in G3]

meet_scalr [in G3]

meet_scalr [in Grassmann]

meet0 [in Grassmann]

meet0l [in Grassmann]

meet0r [in Grassmann]

meet1l [in Grassmann]

meet1r [in Grassmann]

minus_minus_le [in Aux]

minus_match [in Aux]

minus0_le [in Aux]

mk_tuplel_c [in tuple3]

mk_tupler_c [in tuple3]

mprod_S [in VectorSpace]

mprod_2l [in Grassmann]

mprod_app [in VectorSpace]

mprod_hom [in Grassmann]

mprod_cbl [in VectorSpace]

mprod_perm [in VectorSpace]

mprod0 [in VectorSpace]

mprod0l [in VectorSpace]

mprod0r [in VectorSpace]

multK_swap [in Field]

multK_cancel [in Field]

multK_integral [in Field]

multK_m1_m1 [in Field]

multK0l [in Field]

multK0r [in Field]

multK1r [in Field]

## N

natc_id [in tuple3]natc_correct [in tuple3]

natc_eq [in tuple3]

nfelim_c [in tuple3]

nielim_c [in tuple3]

n_to_K_minus [in Field]

n_to_K1 [in Field]

n_to_K_mult [in Field]

n_to_K_add [in Field]

n_to_K0 [in Field]

## O

one_factor_zero [in Grassmann]one_factor_hom [in Grassmann]

one_factor0 [in Grassmann]

online_def [in G3]

oppk [in Grassmann]

oppKl [in Field]

oppK0 [in Field]

opp_multK1l [in Field]

opp_oppK [in Field]

opp_multKl [in Field]

opp_multKr [in Field]

opp_addK [in Field]

opp_multK1r [in Field]

## P

Pappus [in G3]perm_sym [in Aux]

perm_incl_inv [in Aux]

perm_length [in Aux]

perm_in_inv [in Aux]

perm_incl_l [in Aux]

perm_cons_app [in Aux]

perm_incl_r [in Aux]

perm_in [in Aux]

prod_scal_scalr [in Clifford]

prod_scal0r [in Clifford]

prod_scal_addr [in Clifford]

prod_scal0l [in Clifford]

prod_scal_addl [in Clifford]

prod_scal_sym [in Clifford]

prod_scal_scall [in Clifford]

projn [in Grassmann]

proj_lt [in Grassmann]

proj_hom0_eq [in Grassmann]

proj_homk [in Grassmann]

proj_add [in Kn]

proj_scal [in Kn]

proj_base_length [in Grassmann]

proj_e [in Kn]

proj_homn_eq [in Grassmann]

proj0 [in Kn]

proj0 [in Grassmann]

pscal_com [in Kn]

pscal_addl [in Kn]

pscal_e [in Kn]

pscal_meet [in Grassmann]

pscal_addr [in Kn]

pscal_scall [in Kn]

pscal_scalr [in Kn]

pscal_join [in Grassmann]

pscal0l [in Kn]

pscal0r [in Kn]

pseudo_invE [in Clifford]

## R

reorder_c [in tuple3]resolve_c [in tuple3]

revk [in Clifford]

rev_join [in Clifford]

rev_add [in Clifford]

rev_hom [in Clifford]

rev_invo [in Clifford]

rev_scal [in Clifford]

rev_conj [in Clifford]

rev0 [in Clifford]

## S

scalE_mprod [in VectorSpace]scalE_swap [in VectorSpace]

scalE_add0 [in VectorSpace]

scalE_opp [in VectorSpace]

scalE_integral [in VectorSpace]

scalE0r [in VectorSpace]

scalk [in Grassmann]

scal_addE0 [in VectorSpace]

scal_integral [in Kn]

scal_hom [in Grassmann]

scal_integral [in Grassmann]

scmp_c [in tuple3]

splitll [in Grassmann]

splitlr [in Grassmann]

splitrl [in Grassmann]

splitrr [in Grassmann]

splitrr [in G3]

split_meetl [in G3]

split_meetr [in G3]

split3b [in G3]

split3b_v2 [in G3]

split3b_v1 [in G3]

split3l [in G3]

step_c [in tuple3]

sub_add [in G3]

sub_add [in Grassmann]

sub0l [in Grassmann]

sub0r [in Grassmann]

sumEl [in Grassmann]

sumEr [in Grassmann]

sum_ext [in Grassmann]

s2km [in tuple3]

s2ko [in tuple3]

## T

tcompare_eq [in tuple3]term_add_c [in tuple3]

term_zerop_c [in tuple3]

term_opp_c [in tuple3]

term_scale_c [in tuple3]

tin_correct [in tuple3]

tsort_c [in tuple3]

tsplit_c [in tuple3]

tsplit3_c [in tuple3]

tsubst_c [in tuple3]

tvcompare_eq [in tuple3]

tvcompare_refl [in tuple3]

tvcompare_inj [in tuple3]

tvcompare_def [in tuple3]

## U

uniq_app_inv_l [in Aux]uniq_app_inv_r [in Aux]

uniq_free [in VectorSpace]

uniq_cons_inv [in Aux]

uniq_perm [in Aux]

## V

vect_hom_induct [in Grassmann]vect_induct [in Grassmann]

v2l_length [in Grassmann]

## Z

Z_to_K_opp [in Field]Z_to_K_minus [in Field]

Z_to_K_mult [in Field]

Z_to_K_pos [in Field]

Z_to_K_add [in Field]

# Section Index

## E

Exp [in Aux]## F

FF [in tuple3]FF.Examples [in tuple3]

FF.Generic [in tuple3]

FF.NatImplem [in tuple3]

Fold2 [in Aux]

## K

Kn [in Kn]## P

ParamsProp [in Field]Perm [in Aux]

## T

Trans [in VectorSpace]## U

Uniq [in Aux]## V

Vect [in Grassmann]Vect [in G3]

Vect [in Clifford]

VectorSpace [in VectorSpace]

# Notation Index

## E

_ ∨ _ [in Grassmann]_ + _ [in Grassmann]

_ ∧ _ [in Grassmann]

_ .* _ [in Grassmann]

'@ _ [in Grassmann]

[[ X: _ , Y: _ , X**Y: _ ]] [in Grassmann]

_ ∧ _ [in Grassmann]

_ + _ [in Grassmann]

_ .* _ [in Grassmann]

_ ∨ _ [in Grassmann]

'@ _ [in Grassmann]

[[ X: _ , Y: _ , Z: _ , X**Y: _ , Y**Z: _ , X**Z: _ , X**Y**Z: _ ]] [in Grassmann]

_ ∧ _ [in Grassmann]

_ ∨ _ [in Grassmann]

_ + _ [in Grassmann]

_ .* _ [in Grassmann]

#< _ , _ ># [in Grassmann]

'@ _ [in Grassmann]

[[ X: _ , Y: _ , Z: _ , T: _ , X**Y: _ , X**Z: _ , X**T: _ , Y**Z: _ , Y**T: _ , Z**T: _ , X**Y**Z: _ , X**Y**T: _ , X**Z**T: _ , Y**Z**T: _ , X**Y**Z**T: _ , K: _ ]] [in Grassmann]

_ ∧ _ [in Grassmann]

_ .* _ [in Grassmann]

_ ∨ _ [in Grassmann]

_ + _ [in Grassmann]

'@ _ [in Grassmann]

[[ X: _ , Y: _ , Z: _ , T: _ , U: _ , X**Y: _ , X**Z: _ , X**T: _ , X**U: _ , Y**Z: _ , Y**T: _ , Y**U: _ , Z**T: _ , Z**U: _ , T**U: _ , X**Y**Z: _ , X**Y**T: _ , X**Y**U: _ , X**Z**T: _ , X**Z**U: _ , X**T**U: _ , Y**Z**T: _ , Y**Z**U: _ , Y**T**U: _ , Z**T**U: _ , X**Y**Z**T: _ , X**Y**Z**U: _ , X**Y**T**U: _ , X**Z**T**U: _ , Y**Z**T**U: _ , X**Y**Z**T**U: _ , K: _ ]] [in Grassmann]

_ .* _ [in Grassmann]

_ ∧ _ [in Grassmann]

_ ∨ _ [in Grassmann]

_ + _ [in Grassmann]

'@ _ [in Grassmann]

## F

{c[ _ ]} [in tuple3]{e1[ _ ]} [in tuple3]

{e[ _ ]} [in tuple3]

{k[ _ ]} [in tuple3]

{l[ _ ]} [in tuple3]

{t[ _ ]} [in tuple3]

{v[ _ ]} [in tuple3]

{c[ _ ]} [in tuple3]

{k[ _ ]} [in tuple3]

{m[ _ ]} [in tuple3]

{vs[ _ ]} [in tuple3]

{ _ , _ , _ } [in tuple3]

## K

_ [.] _ (kn_scope) [in Kn]'e_ _ (kn_scope) [in Kn]

[ _ ] (kn_scope) [in Kn]

_ [*] _ [in Kn]

K [in Kn]

## P

_ ^ _ (field_scope) [in Field]## V

_ *X* _ (vector_scope) [in VectorSpace]_ ?= 0 (g_scope) [in Grassmann]

K (g_scope) [in Clifford]

1 (g_scope) [in Grassmann]

[ _ ] (g_scope) [in Grassmann]

K (g_scope) [in Grassmann]

_ ^'dl (g_scope) [in Grassmann]

_ ^'l (g_scope) [in Grassmann]

'e_ _ (g_scope) [in Grassmann]

_ - _ (g_scope) [in Grassmann]

_ .* _ (Kn_scope) [in Clifford]

_ ∨ _ (type_scope) [in Grassmann]

_ .* _ [in Clifford]

_ ^d_ _ [in Grassmann]

_ ∧ _ [in G3]

_ ^_'f [in Grassmann]

_ + _ [in Clifford]

_ ?= _ [in G3]

_ ^_'t [in Grassmann]

_ [* _ ] _ [in Clifford]

_ ^_'f [in Clifford]

_ [. _ ] _ [in Clifford]

_ ^d_'f [in Grassmann]

_ + _ [in G3]

_ ∧ _ [in Grassmann]

_ 'L[ _ ] _ [in Clifford]

_ ^_ _ [in Grassmann]

_ - _ [in G3]

_ ∨ _ [in G3]

_ ^d_'t [in Grassmann]

_ ∧ _ [in Clifford]

_ .* _ [in G3]

E [in G3]

E [in G3]

E [in Grassmann]

kn [in Grassmann]

#< _ , _ ># [in Grassmann]

#< _ , _ ># [in Clifford]

#<< _ , _ >># [in Grassmann]

'C[ _ ] [in G3]

'C[ _ ] [in Grassmann]

'C[ _ ] [in Clifford]

'dC[ _ ] [in G3]

'dC[ _ ] [in Grassmann]

'e_ _ [in Clifford]

'kn _ [in Grassmann]

'Pi[ _ ] [in Clifford]

'P[ _ ] [in Clifford]

'R[ _ ] [in Clifford]

'v_ _ [in Clifford]

'v_ _ [in Grassmann]

'@ _ [in Clifford]

'@ _ [in Grassmann]

'@ _ [in G3]

'[ _ , _ , _ ] [in G3]

0 [in G3]

1 [in G3]

[ _ ] [in Clifford]

## other

0 (field_scope) [in Field]_ + _ (field_scope) [in Field]

1 (field_scope) [in Field]

_ ^-1 (field_scope) [in Field]

_ ^ _ (field_scope) [in Field]

_ * _ (field_scope) [in Field]

_ ?= _ (field_scope) [in Field]

- _ (field_scope) [in Field]

[ _ ] (Gn_scope) [in Grassmann]

'e_ _ (Gn_scope) [in Grassmann]

_ [*] _ (Kn_scope) [in Kn]

_ [.] _ (Kn_scope) [in Kn]

[ _ ] (Kn_scope) [in Kn]

'e_ _ (Kn_scope) [in Kn]

_ ?= _ (nat_scope) [in Aux]

_ .+2 (nat_scope) [in Aux]

_ .+1 (nat_scope) [in Aux]

_ .* _ (vector_scope) [in VectorSpace]

0 (vector_scope) [in VectorSpace]

_ ?= _ (vector_scope) [in VectorSpace]

_ + _ (vector_scope) [in VectorSpace]

_ *X* _ (vector_scope) [in VectorSpace]

_ ∨ _ [in G3]

_ is_the_intersection_of [ _ , _ ] and [ _ , _ ] [in G3]

_ .* _ [in G3]

_ + _ [in G3]

_ ?= _ [in G3]

_ - _ [in G3]

_ ∧ _ [in G3]

_ :=: xfree on [ _ , _ ] ( _ , _ ) [in G3]

_ is_free_on [ _ , _ ] [in G3]

E [in G3]

'C[ _ ] [in G3]

'dC[ _ ] [in G3]

'@ _ [in G3]

'[ _ , _ , _ ] [in G3]

0 [in G3]

1 [in G3]

[ _ , _ , _ ] are_collinear [in G3]

# Constructor Index

## C

cbl_add [in Grassmann]cbl_join [in Grassmann]

cbl_scal [in Grassmann]

cbl_in [in VectorSpace]

cbl_in [in Grassmann]

cbl_scal [in VectorSpace]

cbl_add [in VectorSpace]

cbl0 [in VectorSpace]

## E

eql_t0Nr [in Kn]eql_t0Nl [in Kn]

eql_t0N [in Kn]

eql_t0R [in Kn]

eq_Spect [in Aux]

eq_nat_specb [in Aux]

eq_Specf [in Aux]

eq_nat_spect [in Aux]

## I

Inter [in tuple3]## M

More [in tuple3]## P

perm_trans [in Aux]perm_skip [in Aux]

perm_id [in Aux]

perm_swap [in Aux]

## R

RBfalse [in tuple3]RBtrue [in tuple3]

## S

SFree [in tuple3]Sm1 [in tuple3]

SProd [in tuple3]

Stop [in tuple3]

S0 [in tuple3]

S1 [in tuple3]

## T

Tuple [in tuple3]## U

uniq_nil [in Aux]uniq_cons [in Aux]

# Inductive Index

## A

action [in tuple3]## C

cbl [in Grassmann]cbl [in VectorSpace]

## E

eql_t0 [in Kn]eq_nat_spec [in Aux]

eq_Spec [in Aux]

## P

perm [in Aux]## R

rp [in tuple3]## S

sign [in tuple3]sprod [in tuple3]

## T

TBool [in tuple3]tuple [in tuple3]

## U

uniq [in Aux]# Abbreviation Index

## E

E [in Clifford]## G

gvp [in Clifford]## H

hom [in Clifford]## K

kn [in Clifford]## L

liftk [in Grassmann]## P

projk [in Clifford]projk [in Grassmann]

## V

vect [in Clifford]# Definition Index

## A

all [in Grassmann]all_hom1 [in Grassmann]

## B

base [in Grassmann]bin [in Aux]

bracket [in G3]

b2Prop [in Aux]

## C

cadd [in tuple3]ccmp [in tuple3]

ccons [in tuple3]

cdual [in Clifford]

cliff_star [in Clifford]

cliff_starb [in Clifford]

coef [in tuple3]

collinear [in G3]

concur [in G3]

conep [in tuple3]

const [in Grassmann]

contraction_rule [in tuple3]

copp [in tuple3]

cscale [in tuple3]

czerop [in tuple3]

c0 [in tuple3]

c1 [in tuple3]

## D

dconst [in Grassmann]decomposable [in Grassmann]

decompose [in Grassmann]

decomposek [in Grassmann]

delta [in tuple3]

dhead [in Aux]

dlift [in Grassmann]

do_auto [in tuple3]

do_elim [in tuple3]

do_contra [in tuple3]

do_free [in tuple3]

dual [in Grassmann]

## E

ecompare [in tuple3]edelta [in tuple3]

einsert [in tuple3]

einsert0 [in tuple3]

elsprod [in tuple3]

eq_nat [in Aux]

eremove [in tuple3]

esprod [in tuple3]

etsort [in tuple3]

Ex2D.X [in Grassmann]

Ex2D.Y [in Grassmann]

ex21_proof [in tuple3]

Ex3D.X [in Grassmann]

Ex3D.Y [in Grassmann]

Ex3D.Z [in Grassmann]

Ex4D.fxt [in Grassmann]

Ex4D.fxy [in Grassmann]

Ex4D.fxz [in Grassmann]

Ex4D.fyt [in Grassmann]

Ex4D.fyz [in Grassmann]

Ex4D.fzt [in Grassmann]

Ex4D.T [in Grassmann]

Ex4D.T' [in Grassmann]

Ex4D.U [in Grassmann]

Ex4D.X [in Grassmann]

Ex4D.X' [in Grassmann]

Ex4D.Y [in Grassmann]

Ex4D.Y' [in Grassmann]

Ex4D.Z [in Grassmann]

Ex4D.Z' [in Grassmann]

Ex5D.T [in Grassmann]

Ex5D.U [in Grassmann]

Ex5D.X [in Grassmann]

Ex5D.Y [in Grassmann]

Ex5D.Z [in Grassmann]

Ex6D.K [in Grassmann]

Ex6D.T [in Grassmann]

Ex6D.U [in Grassmann]

Ex6D.X [in Grassmann]

Ex6D.Y [in Grassmann]

Ex6D.Z [in Grassmann]

ex7_proof [in tuple3]

## F

f [in Grassmann]f [in Kn]

factor [in Grassmann]

fbracket [in G3]

felim [in tuple3]

fget [in Grassmann]

fn [in Grassmann]

fn [in Kn]

fortho [in Grassmann]

free [in VectorSpace]

free_elim [in tuple3]

## G

gprod [in Clifford]grade [in Grassmann]

## H

has_delta [in tuple3]hom [in G3]

## I

ielim [in tuple3]intera [in tuple3]

interc [in tuple3]

intere [in tuple3]

intere1 [in tuple3]

interl [in tuple3]

interla [in tuple3]

interla_refine [in tuple3]

interm [in tuple3]

intersection [in G3]

intert [in tuple3]

intervs [in tuple3]

inter_elim [in tuple3]

inter_lines [in G3]

is_vector_space [in Grassmann]

is_decomposable [in Grassmann]

is_base [in VectorSpace]

is_vector [in Grassmann]

iter [in Aux]

iter_free [in tuple3]

iter_contra [in tuple3]

iter_split [in tuple3]

iter_rp [in tuple3]

iter_elim [in tuple3]

iter_step [in tuple3]

## J

join [in Grassmann]joinl [in Grassmann]

## K

Kadd [in Kn]Keq [in Kn]

Kgen [in Kn]

Kn [in Kn]

Kn [in Grassmann]

kn2l [in Kn]

kprod [in Kn]

Kproj [in Kn]

Kscal [in Kn]

Ksprod [in Kn]

K0 [in Kn]

K1 [in Clifford]

K1 [in Grassmann]

K2G [in Grassmann]

## L

lcompare [in tuple3]lift [in Grassmann]

lift [in Kn]

line [in G3]

linsert [in tuple3]

list_compare [in tuple3]

list_insert [in tuple3]

lrev [in tuple3]

lsort [in tuple3]

ltsort [in tuple3]

l_contra [in Clifford]

## M

mcontra [in Grassmann]meet [in Grassmann]

mk_tuplel [in tuple3]

mk_tupler [in tuple3]

mprod [in VectorSpace]

## N

natc [in tuple3]ndo_auto [in tuple3]

ndo_auto_c [in tuple3]

nfelim [in tuple3]

nielim [in tuple3]

n_to_K [in Field]

## O

one_factor [in Grassmann]online [in G3]

online1 [in G3]

## P

point [in G3]Pp [in G3]

Pp [in tuple3]

prodk [in Clifford]

prod_scal [in Clifford]

proj [in Grassmann]

proj [in Kn]

pscal [in Kn]

pseudo_inv [in Clifford]

p2v [in G3]

## Q

Qparams [in Grassmann]## R

reorder [in tuple3]resolve [in tuple3]

rev [in tuple3]

rev [in Clifford]

rp_val [in tuple3]

## S

scmp [in tuple3]smult [in tuple3]

smult3 [in tuple3]

sopp [in tuple3]

step [in tuple3]

s2k [in tuple3]

## T

tcompare [in tuple3]term [in tuple3]

term_opp [in tuple3]

term_cmp [in tuple3]

term_zerop [in tuple3]

term_scale [in tuple3]

term_add [in tuple3]

tin [in tuple3]

tsort [in tuple3]

tsplit [in tuple3]

tsplit3 [in tuple3]

tsubst [in tuple3]

tvar [in tuple3]

tvarn [in tuple3]

tvcompare [in tuple3]

## V

Vadd [in Grassmann]Vadd [in G3]

var [in tuple3]

Vconj [in Grassmann]

Vcontra [in Grassmann]

Vdecompose [in Grassmann]

Vdual [in Grassmann]

Vdual [in G3]

vect [in G3]

Vect [in Grassmann]

Veq [in G3]

Veq [in Grassmann]

Vgen [in Grassmann]

Vgenk [in Grassmann]

Vgenk [in G3]

Vjoin [in Grassmann]

Vjoin [in G3]

Vmeet [in Grassmann]

Vmeet [in G3]

vn_eparams [in Kn]

vn_eparams [in Clifford]

vn_eparams [in Grassmann]

Vscal [in G3]

Vscal [in Grassmann]

Vsub [in G3]

v_eparams [in Kn]

v_eparams [in Grassmann]

V0 [in Grassmann]

V1 [in Grassmann]

v2k [in Grassmann]

## Z

Z_to_K [in Field]# Module Index

## E

Ex2D [in Grassmann]Ex3D [in Grassmann]

Ex4D [in Grassmann]

Ex5D [in Grassmann]

Ex6D [in Grassmann]

# Variable Index

## E

Ex2D.p [in Grassmann]Ex3D.p [in Grassmann]

Ex4D.p [in Grassmann]

Ex5D.p [in Grassmann]

Ex6D.p [in Grassmann]

## F

FF.Examples.ex1 [in tuple3]FF.Examples.ex10_2 [in tuple3]

FF.Examples.ex10_1 [in tuple3]

FF.Examples.ex11 [in tuple3]

FF.Examples.ex12 [in tuple3]

FF.Examples.ex13 [in tuple3]

FF.Examples.ex14 [in tuple3]

FF.Examples.ex15 [in tuple3]

FF.Examples.ex16 [in tuple3]

FF.Examples.ex17 [in tuple3]

FF.Examples.ex18 [in tuple3]

FF.Examples.ex19 [in tuple3]

FF.Examples.ex2 [in tuple3]

FF.Examples.ex20 [in tuple3]

FF.Examples.ex21 [in tuple3]

FF.Examples.ex3 [in tuple3]

FF.Examples.ex4 [in tuple3]

FF.Examples.ex5 [in tuple3]

FF.Examples.ex6 [in tuple3]

FF.Examples.ex7 [in tuple3]

FF.Examples.ex8 [in tuple3]

FF.Examples.ex9_3 [in tuple3]

FF.Examples.ex9_1 [in tuple3]

FF.Examples.ex9_2 [in tuple3]

FF.FT [in tuple3]

FF.Generic.cadd [in tuple3]

FF.Generic.cadd_c [in tuple3]

FF.Generic.coef [in tuple3]

FF.Generic.cone [in tuple3]

FF.Generic.conep [in tuple3]

FF.Generic.conep_c [in tuple3]

FF.Generic.cone_c [in tuple3]

FF.Generic.copp [in tuple3]

FF.Generic.copp_c [in tuple3]

FF.Generic.cscale [in tuple3]

FF.Generic.cscale_c [in tuple3]

FF.Generic.czero [in tuple3]

FF.Generic.czerop [in tuple3]

FF.Generic.czerop_c [in tuple3]

FF.Generic.czero_c [in tuple3]

FF.Generic.expr [in tuple3]

FF.Generic.interc [in tuple3]

FF.Generic.interk [in tuple3]

FF.Generic.interv [in tuple3]

FF.Generic.line [in tuple3]

FF.Generic.tvar [in tuple3]

FF.Generic.tvarn [in tuple3]

FF.Generic.tvcompare [in tuple3]

FF.Generic.tvcompare_inj [in tuple3]

FF.Generic.tvcompare_def [in tuple3]

FF.Generic.var [in tuple3]

FF.HP [in tuple3]

FF.K [in tuple3]

FF.NatImplem.interk [in tuple3]

Fold2.A [in Aux]

Fold2.B [in Aux]

Fold2.C [in Aux]

Fold2.f [in Aux]

Fold2.g [in Aux]

## K

Kn.Hp [in Kn]Kn.p [in Kn]

## P

ParamsProp.Hp [in Field]ParamsProp.p [in Field]

Perm.A [in Aux]

## T

Trans.f [in VectorSpace]Trans.g [in VectorSpace]

Trans.g1 [in VectorSpace]

Trans.Hf0 [in VectorSpace]

Trans.Hf1 [in VectorSpace]

Trans.Hf2 [in VectorSpace]

Trans.Hg [in VectorSpace]

Trans.Hp [in VectorSpace]

Trans.Hp1 [in VectorSpace]

Trans.p [in VectorSpace]

Trans.p1 [in VectorSpace]

## U

Uniq.A [in Aux]## V

VectorSpace.Hp [in VectorSpace]VectorSpace.p [in VectorSpace]

VectorSpace.sfP [in VectorSpace]

Vect.add_com [in G3]

Vect.add_assoc [in G3]

Vect.add0l [in G3]

Vect.add0r [in G3]

Vect.F [in G3]

Vect.FT [in G3]

Vect.Hp [in Clifford]

Vect.HP [in G3]

Vect.Hp [in Grassmann]

Vect.join_assoc [in G3]

Vect.join_id [in G3]

Vect.join0l [in G3]

Vect.join0r [in G3]

Vect.meet_assoc [in G3]

Vect.meet_alll [in G3]

Vect.meet_allr [in G3]

Vect.p [in Grassmann]

Vect.p [in Clifford]

Vect.scal_addr [in G3]

Vect.scal_addl [in G3]

Vect.scal_integral [in G3]

Vect.scal_mult [in G3]

Vect.scal_mul [in G3]

Vect.scal0l [in G3]

Vect.scal0r [in G3]

Vect.scal1l [in G3]

# Library Index

## A

Aux## C

Clifford## F

Field## G

GrassmannG3

## K

Kn## T

tuple3## V

VectorSpaceGlobal Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1305 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (37 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (700 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |

Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (145 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (33 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (226 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (110 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |

This page has been generated by coqdoc