Documentation
Monlib
.
LinearAlgebra
.
Matrix
.
Cast
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
j
:
k
}
(
x
:
Matrix
(
s
i
)
(
s
i
)
R
)
(
h
:
i
=
j
)
(
p
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
j
:
k
}
(
x
:
Matrix
(
s
j
)
(
s
j
)
R
)
(
h
:
j
=
i
)
(
p
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
j
:
k
}
(
x
y
:
Matrix
(
s
i
)
(
s
i
)
R
)
(
h
:
i
=
j
)
:
⋯
.
mp
(
x
*
y
)
=
⋯
.
mp
x
*
⋯
.
mp
y