Documentation
Monlib
.
LinearAlgebra
.
Matrix
.
Cast
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Matrix.Basic
Imported by
Matrix
.
cast_apply
Matrix
.
cast_apply'
Matrix
.
cast_hMul
source
theorem
Matrix
.
cast_apply
{R :
Type
u_1}
{k :
Type
u_2}
{s :
k
→
Type
u_3
}
{i :
k
}
{j :
k
}
(x :
Matrix
(
s
i
)
(
s
i
)
R
)
(h :
i
=
j
)
(p :
s
j
)
(q :
s
j
)
:
⋯
.mp
x
p
q
=
x
(
⋯
.mpr
p
)
(
⋯
.mpr
q
)
source
theorem
Matrix
.
cast_apply'
{R :
Type
u_1}
{k :
Type
u_2}
{s :
k
→
Type
u_3
}
{i :
k
}
{j :
k
}
(x :
Matrix
(
s
j
)
(
s
j
)
R
)
(h :
j
=
i
)
(p :
s
i
)
(q :
s
i
)
:
⋯
.mpr
x
p
q
=
x
(
⋯
.mpr
p
)
(
⋯
.mpr
q
)
source
theorem
Matrix
.
cast_hMul
{R :
Type
u_1}
{k :
Type
u_2}
{s :
k
→
Type
u_3
}
[
Semiring
R
]
[
(
i
:
k
) →
Fintype
(
s
i
)
]
{i :
k
}
{j :
k
}
(x :
Matrix
(
s
i
)
(
s
i
)
R
)
(y :
Matrix
(
s
i
)
(
s
i
)
R
)
(h :
i
=
j
)
:
⋯
.mp
(
x
*
y
)
=
⋯
.mp
x
*
⋯
.mp
y