HOL html
| Files 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 | _ |
| Theorems 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 | _ |
C (theorems)
CART_EQ3CCROSS_COLLINEAR_CVECTORS
CCROSS_COMPONENT
CCROSS_JACOBI
CCROSS_LADD
CCROSS_LMUL
CCROSS_LNEG
CCROSS_LREAL
CCROSS_LZERO
CCROSS_RADD
CCROSS_REFL
CCROSS_RMUL
CCROSS_RNEG
CCROSS_RREAL
CCROSS_RZERO
CCROSS_SKEW
CDOT3
CDOT_CAUCHY_SCHWARZ
CDOT_CAUCHY_SCHWARZ_EQUAL
CDOT_CAUCHY_SCHWARZ_POW_2
CDOT_CAUCHY_SCHWARZ_POW_2_EQUAL
CDOT_CUNIT_MUL_CUNIT
CDOT_EQ_0
CDOT_LADD
CDOT_LMUL
CDOT_LNEG
CDOT_LREAL
CDOT_LSUB
CDOT_LZERO
CDOT_PYTHAGOREAN
CDOT_RADD
CDOT_RMUL
CDOT_RNEG
CDOT_RREAL
CDOT_RSUB
CDOT_RZERO
CDOT_SELF_POS
CDOT_SYM
CINFSUM_LINEAR
CLINEAR_0
CLINEAR_ADD
CLINEAR_CMUL
CLINEAR_COMPOSE
CLINEAR_COMPOSE_ADD
CLINEAR_COMPOSE_CMUL
CLINEAR_COMPOSE_NEG
CLINEAR_COMPOSE_SUB
CLINEAR_FSTCART_SNDCART
CLINEAR_I
CLINEAR_ID
CLINEAR_INJECTIVE_0
CLINEAR_NEG
CLINEAR_NEGATION
CLINEAR_SUB
CLINEAR_VMUL_COMPONENT
CLINEAR_ZERO
CNJ_ZERO
CNORM2_ALT
CNORM2_CVECTOR_ZERO
CNORM2_EQ_0
CNORM2_MODULUS
CNORM2_MUL
CNORM2_NORM2
CNORM2_NORM2_2
CNORM2_POS
CNORM2_SUB
CNORM2_VECTOR_TO_CVECTOR
CNORM_BASIS
CNORM_BASIS_1
CNORM_CVECTOR_ZERO
CNORM_EQ_0
CNORM_MUL
CNORM_NORM
CNORM_NORM_2
CNORM_POS
CNORM_POW_2
CNORM_SUB
CNORM_TRIANGLE
CNORM_VECTOR_TO_CVECTOR
COLLINEAR_CVECTORS_0
COLLINEAR_CVECTORS_SYM
COLLINEAR_CVECTORS_VECTOR_TO_CVECTOR
COLLINEAR_DEPENDENT
COLLINEAR_LNONNULL
COLLINEAR_RNONNULL
COLLINEAR_RUNITREAL
COLLINEAR_UNIT
COLLINEAR_VEC0
COMPLEX_ADD_IS_A_MAP
COMPLEX_ADD_POW_2
COMPLEX_BALANCE_DIV_MUL
COMPLEX_BALANCE_MUL_DIV
COMPLEX_MUL_LINV2
COMPLEX_NEG_IS_A_MAP
COMPLEX_SUB_IS_A_MAP
COMPLEX_VECTOR_MAP
COMPLEX_VECTOR_MAP2
COMPLEX_VECTOR_TRANSPOSE
COMPONENT_LE_NORM_ALT
CORTHOGONAL_0
CORTHOGONAL_COLLINEAR_CVECTORS
CORTHOGONAL_LRMUL_CLAUSES
CORTHOGONAL_MUL_CLAUSES
CORTHOGONAL_PROJECTION
CORTHOGONAL_REAL_CLAUSES
CORTHOGONAL_SYM
CORTHOGONAL_UNIT
CROSS_NORM_ORTHOGONAL
CSQRT_MUL_LCX
CSQRT_MUL_LCX_LT
CSUMMABLE_FLATTEN_CVECTOR
CSUMMABLE_LINEAR
CUNIT_CVECTOR_ZERO
CVECTOR_ADD_AC
CVECTOR_ADD_ALT
CVECTOR_ADD_COMPONENT
CVECTOR_CHOOSE_SIZE
CVECTOR_EQ
CVECTOR_IM_ADD
CVECTOR_IM_CNJ
CVECTOR_IM_COMPONENT
CVECTOR_IM_MUL
CVECTOR_IM_VECTOR_MAP
CVECTOR_IM_VECTOR_MAP2
CVECTOR_IM_VECTOR_TO_CVECTOR
CVECTOR_IM_VECTOR_TO_CVECTOR_IM
CVECTOR_IM_VECTOR_TO_CVECTOR_RE_IM
CVECTOR_MUL_COMPONENT
CVECTOR_MUL_EQ_0
CVECTOR_MUL_INV
CVECTOR_MUL_INV2
CVECTOR_MUL_LCANCEL
CVECTOR_MUL_RCANCEL
CVECTOR_NEG_ALT
CVECTOR_NEG_COMPONENT
CVECTOR_NON_ZERO
CVECTOR_RE_ADD
CVECTOR_RE_COMPONENT
CVECTOR_RE_MUL
CVECTOR_RE_VECTOR_MAP
CVECTOR_RE_VECTOR_MAP2
CVECTOR_RE_VECTOR_TO_CVECTOR
CVECTOR_RE_VECTOR_TO_CVECTOR_RE_IM
CVECTOR_SUB_ALT
CVECTOR_SUB_COMPONENT
CVECTOR_ZERO_COMPONENT
CVECTOR_ZERO_VEC0
CX_CNORM2
ccross
cdot
cinfsum
clinear
cnorm
cnorm2
collinear_cvectors
complex_vector
corthogonal
csummable
cunit
cvector_add
cvector_cnj
cvector_flatten
cvector_im
cvector_mul
cvector_neg
cvector_re
cvector_sub
cvector_unflatten
cvector_zero
cvsum