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
AuxC
CliffordF
FieldG
GrassmannG3
K
KnT
tuple3V
VectorSpace| 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) |
This page has been generated by coqdoc