Matrix.IsSymm.ext_iff
theorem Matrix.IsSymm.ext_iff :
∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, A.IsSymm ↔ ∀ (i j : n), A j i = A i j
This theorem states that for any type `α` and any index type `n`, a matrix `A` of elements of type `α` with indices from `n` is symmetric (i.e., `A` is identical to its own transpose) if and only if for all indices `i` and `j` in `n`, the element at row `j` and column `i` of `A` is equal to the element at row `i` and column `j` of `A`. In mathematical terms, this corresponds to the statement that a matrix is symmetric if and only if `A_{j,i} = A_{i,j}` for all `i` and `j`.
More concisely: A square matrix over a type `α` is symmetric if and only if its transpose is equal to the matrix itself, i.e., `A = A.transpose`. Equivalently, the element at row `i` and column `j` is equal to the element at row `j` and column `i` for all indices `i` and `j`, i.e., `A_{i,j} = A_{j,i}`.
|
Matrix.isSymm_fromBlocks_iff
theorem Matrix.isSymm_fromBlocks_iff :
∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
{D : Matrix n n α}, (A.fromBlocks B C D).IsSymm ↔ A.IsSymm ∧ B.transpose = C ∧ C.transpose = B ∧ D.IsSymm
This theorem states that for any types `α`, `n`, `m` and matrices `A` of type `Matrix m m α`, `B` of type `Matrix m n α`, `C` of type `Matrix n m α`, and `D` of type `Matrix n n α`, the block matrix formed from `A`, `B`, `C`, and `D` is symmetric if and only if `A` is symmetric, `B` is the transpose of `C`, `C` is the transpose of `B`, and `D` is symmetric. In mathematical terms, a block matrix $\begin{bmatrix} A & B \\ C & D \end{bmatrix}$ is symmetric if and only if $A$ and $D$ are symmetric and $B$ and $C$ are each other's transposes.
More concisely: A block matrix $\begin{bmatrix} A & B \\ C & D \end{bmatrix}$ is symmetric if and only if $A$ and $D$ are symmetric, and $B$ is the transpose of $C$ (equivalently, $C$ is the transpose of $B$).
|
Matrix.IsSymm.fromBlocks
theorem Matrix.IsSymm.fromBlocks :
∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
{D : Matrix n n α}, A.IsSymm → B.transpose = C → D.IsSymm → (A.fromBlocks B C D).IsSymm
The theorem `Matrix.IsSymm.fromBlocks` asserts that a block matrix, represented by `A.fromBlocks B C D`, is symmetric if and only if the following conditions are met: Matrix `A` and Matrix `D` are both symmetric, and the transpose of Matrix `B` is equal to Matrix `C`. Here symmetric means a matrix is equal to its transpose, and `A.fromBlocks B C D` represents a block matrix constructed from matrices `A`, `B`, `C`, and `D`. The matrices `A` and `D` are square matrices indexed by types `m` and `n` respectively, while `B` and `C` are rectangular matrices linking the two types. The entries of the matrices are from an arbitrary type `α`.
More concisely: A block matrix `A.fromBlocks B C D` is symmetric if and only if matrices `A` and `D` are symmetric and matrix `B` is equal to the transpose of matrix `C`.
|
Matrix.isSymm_diagonal
theorem Matrix.isSymm_diagonal :
∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : Zero α] (v : n → α), (Matrix.diagonal v).IsSymm
This theorem states that for any type `α` and another type `n`, given that `α` has an instance of zero and equality on `n` is decidable, for any function `v` mapping `n` to `α`, the diagonal matrix created using `v` is symmetric. In other words, for a given function `v : n → α`, the diagonal matrix `diagonal v` is such that its entry at position `(i, j)` is equal to its entry at position `(j, i)` for all `i` and `j` in `n`. This means that the matrix is symmetric about its main diagonal.
More concisely: For any function `v : n -> alpha` from a type `n` to a type `alpha` with zero and decidable equality, the diagonal matrix `diagonal v` is symmetric.
|
Matrix.IsSymm.ext
theorem Matrix.IsSymm.ext :
∀ {α : Type u_1} {n : Type u_3} {A : Matrix n n α}, (∀ (i j : n), A j i = A i j) → A.IsSymm
The theorem `Matrix.IsSymm.ext` states that for any type `α` and indexing type `n`, given a square matrix `A` of type `α` indexed by `n`, if for all indices `i` and `j` of type `n`, the element at position `(j, i)` is equal to the element at position `(i, j)` (i.e., the matrix is symmetrical along its main diagonal), then `A` is symmetric, as defined by the `IsSymm` property of `Matrix`.
More concisely: If a square matrix is equal to its transpose, then it is symmetric.
|