:: MATRIX17 semantic presentation begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M" is :::"subsymmetric"::: means :: MATRIX17:def 1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))); end; :: deftheorem defines :::"subsymmetric"::: MATRIX17:def 1 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_matrix17 :::"subsymmetric"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) "a") -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_matrix_1 :::"tabular"::: ) ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v1_matrix17 :::"subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set ($#k2_matrix_3 :::"-"::: ) "M") -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v1_matrix17 :::"subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M1" ($#k3_matrix_3 :::"+"::: ) "M2") -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "M" be ($#v1_matrix17 :::"subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "a" ($#k6_matrix_3 :::"*"::: ) "M") -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v1_matrix17 :::"subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set bbbadK1_MATRIX_4("K" "," "M1" "," "M2")) -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v1_matrix17 :::"subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_matrix16 :::"line_circulant"::: ) -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); cluster ($#v3_matrix16 :::"col_circulant"::: ) -> ($#v1_matrix17 :::"subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M" is :::"Anti-subsymmetric"::: means :: MATRIX17:def 2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )))); end; :: deftheorem defines :::"Anti-subsymmetric"::: MATRIX17:def 2 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ")" )))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_matrix_1 :::"tabular"::: ) ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; theorem :: MATRIX17:1 (Bool "for" (Set (Var "K")) "being" ($#v12_vectsp_1 :::"Fanoian"::: ) ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M1")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")))) & (Bool (Set (Var "M1")) "is" ($#v2_matrix17 :::"Anti-subsymmetric"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set ($#k2_matrix_3 :::"-"::: ) "M") -> ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M1" ($#k3_matrix_3 :::"+"::: ) "M2") -> ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "M" be ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "a" ($#k6_matrix_3 :::"*"::: ) "M") -> ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set bbbadK1_MATRIX_4("K" "," "M1" "," "M2")) -> ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v2_matrix17 :::"Anti-subsymmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v2_matrix17 :::"Anti-subsymmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; begin definitionlet "K" be ($#l6_algstr_0 :::"Field":::); let "n" be ($#m1_hidden :::"Nat":::); let "M" be ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); attr "M" is :::"central_symmetric"::: means :: MATRIX17:def 3 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j"))))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))); end; :: deftheorem defines :::"central_symmetric"::: MATRIX17:def 3 : (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v3_matrix17 :::"central_symmetric"::: ) ) "iff" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "," (Set (Var "l")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")))) & (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "k")) "," (Set (Var "l")) ")" ))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) "a") -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_matrix_1 :::"tabular"::: ) ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v3_matrix17 :::"central_symmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set ($#k2_matrix_3 :::"-"::: ) "M") -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v3_matrix17 :::"central_symmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M1" ($#k3_matrix_3 :::"+"::: ) "M2") -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "M" be ($#v3_matrix17 :::"central_symmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "a" ($#k6_matrix_3 :::"*"::: ) "M") -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v3_matrix17 :::"central_symmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set bbbadK1_MATRIX_4("K" "," "M1" "," "M2")) -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M" be ($#v3_matrix17 :::"central_symmetric"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M" ($#k4_matrix_1 :::"@"::: ) ) -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v2_matrix_6 :::"symmetric"::: ) ($#v1_matrix17 :::"subsymmetric"::: ) -> ($#v3_matrix17 :::"central_symmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; begin definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); let "p" be ($#m1_hidden :::"FinSequence":::); pred "M" :::"is_symmetry_circulant_about"::: "p" means :: MATRIX17:def 4 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) "M")) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set "M" ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_symmetry_circulant_about"::: MATRIX17:def 4 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "M")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_matrix_1 :::"Indices"::: ) (Set (Var "M")))) & (Bool (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "M")) ($#k3_matrix_1 :::"*"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" ) ")" ) ")" )))); theorem :: MATRIX17:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set "(" (Set (Var "n")) "," (Set (Var "n")) ")" ($#k2_matrix_2 :::"-->"::: ) (Set (Var "a"))) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Set (Var "n")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a"))))))) ; theorem :: MATRIX17:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set (Var "M1"))) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))))))))) ; theorem :: MATRIX17:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k1_matrix_6 :::"-"::: ) (Set (Var "M1"))) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")))))))) ; theorem :: MATRIX17:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "M1")) "," (Set (Var "M2")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))) & (Bool (Set (Var "M2")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "q")))) "holds" (Bool (Set (Set (Var "M1")) ($#k2_matrix_6 :::"+"::: ) (Set (Var "M2"))) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")))))))) ; definitionlet "K" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Const "K")); attr "M" is :::"symmetry_circulant"::: means :: MATRIX17:def 5 (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" "K" "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) "M")) & (Bool "M" ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))) ")" )); end; :: deftheorem defines :::"symmetry_circulant"::: MATRIX17:def 5 : (Bool "for" (Set (Var "K")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m2_finseq_1 :::"Matrix":::) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v4_matrix17 :::"symmetry_circulant"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_1 :::"width"::: ) (Set (Var "M")))) & (Bool (Set (Var "M")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))) ")" )) ")" ))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); attr "p" is :::"first-symmetry-of-circulant"::: means :: MATRIX17:def 6 (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" "st" (Bool (Set (Var "M")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) "p")); end; :: deftheorem defines :::"first-symmetry-of-circulant"::: MATRIX17:def 6 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) "iff" (Bool "ex" (Set (Var "M")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "st" (Bool (Set (Var "M")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p")))) ")" ))); definitionlet "K" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "K")); assume (Bool (Set (Const "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) ; func :::"SCirc"::: "p" -> ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) "p") "," "K" means :: MATRIX17:def 7 (Bool it ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) "p"); end; :: deftheorem defines :::"SCirc"::: MATRIX17:def 7 : (Bool "for" (Set (Var "K")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) "," (Set (Var "K")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")))) "iff" (Bool (Set (Var "b3")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))) ")" )))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); cluster (Set "(" "n" "," "n" ")" ($#k1_matrix_2 :::"-->"::: ) "a") -> ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() ($#v1_matrix_1 :::"tabular"::: ) ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end; theorem :: MATRIX17:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "A")) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p")))) "holds" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_matrix17 :::"is_symmetry_circulant_about"::: ) (Set (Var "p"))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); let "M1" be ($#v4_matrix17 :::"symmetry_circulant"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "a" ($#k6_matrix_3 :::"*"::: ) "M1") -> ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v4_matrix17 :::"symmetry_circulant"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set "M1" ($#k3_matrix_3 :::"+"::: ) "M2") -> ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1" be ($#v4_matrix17 :::"symmetry_circulant"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set ($#k2_matrix_3 :::"-"::: ) "M1") -> ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); let "M1", "M2" be ($#v4_matrix17 :::"symmetry_circulant"::: ) ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "K")); cluster (Set bbbadK1_MATRIX_4("K" "," "M1" "," "M2")) -> ($#v4_matrix17 :::"symmetry_circulant"::: ) for ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," "K"; end; theorem :: MATRIX17:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_matrix17 :::"symmetry_circulant"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k5_matrix_1 :::"@"::: ) ) "is" ($#v4_matrix17 :::"symmetry_circulant"::: ) )))) ; theorem :: MATRIX17:8 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p"))) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ))) ; theorem :: MATRIX17:9 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix_6 :::"-"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ))))) ; theorem :: MATRIX17:10 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q"))) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ))) ; theorem :: MATRIX17:11 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "q")) ")" ))))) ; theorem :: MATRIX17:12 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )))) ; theorem :: MATRIX17:13 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX17:14 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_matrix_6 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b")) ")" ) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: MATRIX17:15 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX17:16 (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "K")) "st" (Bool (Bool (Set (Var "p")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_matrix17 :::"first-symmetry-of-circulant"::: ) ) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_matrix_3 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k2_matrix13 :::"*"::: ) (Set "(" ($#k1_matrix17 :::"SCirc"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_matrix17 :::"SCirc"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "q")) ")" ) ")" )))))) ; theorem :: MATRIX17:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "K")) "being" ($#l6_algstr_0 :::"Field":::) (Bool "for" (Set (Var "M1")) "being" ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v4_matrix17 :::"symmetry_circulant"::: ) )) "holds" (Bool (Set (Set (Var "M1")) ($#k5_matrix_1 :::"@"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "M1")))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "K" be ($#l6_algstr_0 :::"Field":::); cluster ($#v4_matrix17 :::"symmetry_circulant"::: ) -> ($#v2_matrix_6 :::"symmetric"::: ) for ($#m1_matrix_1 :::"Matrix"::: ) "of" "n" "," "n" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K"); end;