K93() is set
K97() is V11() V24() V25() V26() M2( bool K93())
bool K93() is set
K92() is V11() V24() V25() V26() set
bool K92() is set
bool K97() is set
1 is V11() V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
2 is V11() V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
0 is set
0 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric Matrix of n,n, the U1 of K
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
(1. (K,n)) * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width (0. (K,n,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (0. (K,n,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(0. (K,n,n)) * (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric Matrix of n,n, the U1 of K
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M1 @) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) @) * ((M1 @) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * ((M1 @) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n))) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
- (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 * M1) + (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 + M2) * M1) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M2) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) + (- (M2 * M1)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) + ((M2 * M1) + (- (M2 * M1))) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
(M1 * M1) + (0. (K,n,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 ~) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (((M2 ~) * M1) * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M2 ~) * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M2 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(((M2 ~) * M1) * M2) * (((M2 ~) * M1) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 ~) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M2 ~) * M1) * M2) * ((M2 ~) * (M1 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M2 ~) * M1) * M2) * (M2 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((((M2 ~) * M1) * M2) * (M2 ~)) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (M2 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 ~) * M1) * (M2 * (M2 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M2 ~) * M1) * (M2 * (M2 ~))) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
((M2 ~) * M1) * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M2 ~) * M1) * (1. (K,n))) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 ~) * M1) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 ~) * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M2 ~) * M1) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 ~) * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 ~) * (M1 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 ~) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 ~) * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 ~) * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(1. (K,n)) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 * M2) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M2) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * (M2 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * (M1 * M2)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) * M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width (M1 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 @) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M1 @) * (M2 @)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * (M2 @)) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 @) * (M2 @)) * (M1 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M2 @) * (M1 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * ((M2 @) * (M1 @))) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M2) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M1 * M2) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * ((M1 * M2) @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M2 * M1) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * ((M2 * M1) @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * ((M1 @) * (M2 @))) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * (M1 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 @) * (M1 @)) * (M2 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 * M1) @) * (M2 @)) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 @) * (M2 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M2 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M2) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * ((M2 * M2) @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * (M2 @)) * ((M1 @) * (M2 @)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M2 * M1) * (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 * M1) * M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * (1. (K,n))) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M1 * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * (M1 @)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
((M1 @) * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 @) * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
len M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
(1. (K,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 ~) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 ~) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 ~) * (M1 * M3) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 ~) * M1) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(1. (K,n)) * M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M3 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M3 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M3 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 ~ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 ~) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M2 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (M1 * (M1 ~)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) * (M1 ~) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
(M1 * M2) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M2 * M1) * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * (M1 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * (M1 * M1)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M2 * (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * (0. (K,n))) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(0. (K,n,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n))) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 * M1) + (0. (K,n))) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(0. (K,n)) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M2 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
- (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 + M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M2 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 * M1) + (M2 * M1) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width ((M1 * M1) + (M2 * M1)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M2 * M1) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 * M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width (M1 + M2) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 + M2) * (M1 + M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 + M2) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 + M2) * M1) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + ((M1 + M2) * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M2) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + ((M1 * M2) + (M2 * M2)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (M2 * M1)) + (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(((M1 * M1) + (M2 * M1)) + (M1 * M2)) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M2 * M1) + (- (M2 * M1)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) + ((M2 * M1) + (- (M2 * M1))) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + ((M2 * M1) + (- (M2 * M1)))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) + (0. (K,n,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
((M1 * M1) + (0. (K,n,n))) + (M2 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(0. (K,n)) + (0. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
(M1 @) * (M1 @) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
(0. (K,n)) @ is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(n,n) --> (0. K) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
K179(n,(0. K)) is V1() Function-like FinSequence-like set
K179(n,K179(n,(0. K))) is V1() Function-like FinSequence-like set
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
Indices (1. (K,n)) is set
dom (1. (K,n)) is M2( bool K97())
width (1. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
Seg (width (1. (K,n))) is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (1. (K,n)) ) } is set
[:(dom (1. (K,n))),(Seg (width (1. (K,n)))):] is set
Seg n is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is set
0 + 1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
[1,1] is set
Indices (0. (K,n)) is set
dom (0. (K,n)) is M2( bool K97())
width (0. (K,n)) is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
Seg (width (0. (K,n))) is M2( bool K97())
{ b1 where b1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97()) : ( 1 <= b1 & b1 <= width (0. (K,n)) ) } is set
[:(dom (0. (K,n))),(Seg (width (0. (K,n)))):] is set
(0. (K,n)) * (1,1) is M2( the U1 of K)
1. K is V55(K) M2( the U1 of K)
n is V24() V25() V26() V30() V31() V32() ext-real V113() set
K is V48() V52() non trivial V74() almost_left_invertible V120() V122() V125() V126() V127() well-unital V139() L11()
the U1 of K is V11() non trivial set
K180( the U1 of K) is M8( the U1 of K)
M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
len M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
width M1 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
width M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M2(K97())
len M2 is V24() V25() V26() V30() V31() V32() ext-real V113() M3(K93(),K97())
1. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular symmetric (n,K) (n,K) Matrix of n,n, the U1 of K
M1 * (1. (K,n)) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * (M1 * M2) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
M1 * M1 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
(M1 * M1) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular (n,K) (n,K) Matrix of n,n, the U1 of K
K181(n, the U1 of K) is M8( the U1 of K)
0. K is V55(K) M2( the U1 of K)
K182( the U1 of K,n,(0. K)) is V1() V4(K97()) V5( the U1 of K) Function-like FinSequence-like M9( the U1 of K,K181(n, the U1 of K))
K182(K181(n, the U1 of K),n,K182( the U1 of K,n,(0. K))) is V1() V4(K97()) V5(K181(n, the U1 of K)) Function-like FinSequence-like M9(K181(n, the U1 of K),K181(n,K181(n, the U1 of K)))
K181(n,K181(n, the U1 of K)) is M8(K181(n, the U1 of K))
(0. (K,n)) * M2 is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
0. (K,n,n) is V1() V4(K97()) V5(K180( the U1 of K)) Function-like FinSequence-like tabular Matrix of n,n, the U1 of K
n is V24() V25() V26() V30() V31() V32