Matrix is a signing of another matrix #
This file describes when a matrix is a signing of another matrix.
def
Matrix.IsSigningOf
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[LinearOrderedRing R]
{n : ℕ}
(A : Matrix X Y R)
(U : Matrix X Y (ZMod n))
:
LinearOrderedRing-valued matrix A is a signing of U (matrix of the same size but different type) iff A has
the same entries as U on respective positions up to signs.
Instances For
theorem
Matrix.IsSigningOf.submatrix
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[LinearOrderedRing R]
{n : ℕ}
{X' : Type u_4}
{Y' : Type u_5}
{A : Matrix X Y R}
{U : Matrix X Y (ZMod n)}
(hAU : A.IsSigningOf U)
(f : X' → X)
(g : Y' → Y)
:
(A.submatrix f g).IsSigningOf (U.submatrix f g)
theorem
Matrix.IsSigningOf.reindex
{X : Type u_1}
{Y : Type u_2}
{R : Type u_3}
[LinearOrderedRing R]
{n : ℕ}
{X' : Type u_4}
{Y' : Type u_5}
{A : Matrix X Y R}
{U : Matrix X Y (ZMod n)}
(hAU : A.IsSigningOf U)
(f : X ≃ X')
(g : Y ≃ Y')
:
((Matrix.reindex f g) A).IsSigningOf ((Matrix.reindex f g) U)