Matrix.isDiag_zero
theorem Matrix.isDiag_zero : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α], Matrix.IsDiag 0
The theorem `Matrix.isDiag_zero` states that for any type `α` that has a zero element, and for any type `n`, the zero matrix (a square matrix of type `n` by `n` with all entries being the zero element of type `α`) is a diagonal matrix. A matrix is defined as diagonal using the `Matrix.IsDiag` definition, which states that a square matrix `A` is a diagonal matrix if and only if all its off-diagonal entries are zero.
More concisely: For any type with a zero element and any square matrix over it, the zero matrix is a diagonal matrix with all diagonal entries equal to the zero element.
|
Matrix.IsDiag.kronecker
theorem Matrix.IsDiag.kronecker :
∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : MulZeroClass α] {A : Matrix m m α} {B : Matrix n n α},
A.IsDiag → B.IsDiag → (Matrix.kroneckerMap (fun x x_1 => x * x_1) A B).IsDiag
The theorem `Matrix.IsDiag.kronecker` states that for any type `α` with a multiplication operation that respects zero ("`MulZeroClass α`"), and any matrices `A` and `B` of type `Matrix m m α` and `Matrix n n α` respectively, if both `A` and `B` are diagonal matrices (`A.IsDiag` and `B.IsDiag`), then the Kronecker product of `A` and `B`, which is defined as the matrix obtained by applying the function `(fun x x_1 => x * x_1)` to every pair of elements from `A` and `B`, is also a diagonal matrix (`(Matrix.kroneckerMap (fun x x_1 => x * x_1) A B).IsDiag`).
In mathematical terms, if A and B are diagonal matrices, then the Kronecker product A ⊗ B is also a diagonal matrix.
More concisely: If `A` and `B` are diagonal matrices, then their Kronecker product `A ⊗ B` is also a diagonal matrix.
|
Matrix.IsDiag.diagonal_diag
theorem Matrix.IsDiag.diagonal_diag :
∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : DecidableEq n] {A : Matrix n n α},
A.IsDiag → Matrix.diagonal A.diag = A
This theorem states that for any square matrix `A` of type `Matrix n n α`, where `α` is any type with a defined zero and `n` is any type with decidable equality, if `A` is a diagonal matrix (i.e., all its non-diagonal entries are zero), then the matrix generated using the `Matrix.diagonal` function from the diagonal entries of `A` (obtained using `A.diag`) is equal to `A` itself. In other words, any diagonal matrix can be represented by the `Matrix.diagonal` of its own diagonal entries.
More concisely: For any square matrix `A` of type `Matrix n n α` over a type `α` with a defined zero and `n` having decidable equality, if `A` is a diagonal matrix, then `A` equals the diagonal matrix generated from its own diagonal entries using `Matrix.diagonal` (`A.diag`).
|
Matrix.isDiag_fromBlocks_iff
theorem Matrix.isDiag_fromBlocks_iff :
∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {B : Matrix m n α}
{C : Matrix n m α} {D : Matrix n n α}, (A.fromBlocks B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
The theorem `Matrix.isDiag_fromBlocks_iff` states that for any given types `α`, `n`, and `m`, and any given instances of `Zero α` and matrices `A`, `B`, `C`, and `D` where `A` is a `m x m` matrix, `B` is a `m x n` matrix, `C` is a `n x m` matrix and `D` is a `n x n` matrix with entries in `α`, the block matrix formed from `A`, `B`, `C` and `D` is a diagonal matrix if and only if `A` and `D` are diagonal matrices and `B` and `C` are zero matrices.
More concisely: A block matrix formed by a diagonal matrix `A` of size `m x m`, zero matrix `B` of size `m x n`, matrix `C` of size `n x m`, and diagonal matrix `D` of size `n x n` is diagonal if and only if `A` and `D` are diagonal matrices and `B` and `C` are zero matrices.
|
Matrix.IsDiag.fromBlocks_of_isSymm
theorem Matrix.IsDiag.fromBlocks_of_isSymm :
∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {C : Matrix n m α}
{D : Matrix n n α}, (A.fromBlocks 0 C D).IsSymm → A.IsDiag → D.IsDiag → (A.fromBlocks 0 C D).IsDiag
The theorem states that for any types `α` (assumed to have an addition operation), `n`, and `m`, given matrices `A` of dimensions `m` by `m` and `D` of dimensions `n` by `n` with entries in `α`, and a matrix `C` with dimensions `n` by `m`, the block matrix constructed from `A`, a zero matrix, `C`, and `D` is diagonal if the block matrix is symmetric and both `A` and `D` are diagonal. In other words, a symmetric block matrix consisting of diagonal matrices `A` and `D`, and a zero matrix in place of `B`, is itself a diagonal matrix.
More concisely: If matrices A of dimension m by m, C of dimension n by m, and D of dimension n by n are such that A and D are diagonal, and the block matrix [A | 0\_mxE | C] [C^T | D] is symmetric, then it is a diagonal matrix.
|
Matrix.isDiag_one
theorem Matrix.isDiag_one :
∀ {α : Type u_1} {n : Type u_4} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.IsDiag 1 := by
sorry
This theorem states that every identity matrix is a diagonal matrix. In more detail, for any types α and n where α has a zero and a one (typically representing a numeric type like integers, reals, etc.) and n has a decidable equality (typically representing the indices or dimensions), the identity matrix of size n and entries of type α is a diagonal matrix. A matrix is diagonal if all its off-diagonal entries are zero, which is true for the identity matrix.
More concisely: For any type α with zero and one, and decidable equality index type n, the identity matrix of size n with entries of type α is a diagonal matrix. (In other words, the identity matrix is a matrix with all off-diagonal entries equal to zero.)
|
Matrix.IsDiag.fromBlocks
theorem Matrix.IsDiag.fromBlocks :
∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {D : Matrix n n α},
A.IsDiag → D.IsDiag → (A.fromBlocks 0 0 D).IsDiag
The theorem `Matrix.IsDiag.fromBlocks` asserts that for any types `α`, `n`, and `m`, given an instance of `Zero` for `α`, and matrices `A` and `D` with entries in `α` (where `A` is indexed by `m` and `D` is indexed by `n`), if both `A` and `D` are diagonal matrices, then the block matrix created from `A` and `D` with zero blocks is also a diagonal matrix. In other words, a block matrix composed of diagonal matrices and filled with zeros elsewhere is itself a diagonal matrix.
More concisely: If matrices `A` and `D` are diagonal with entries in a type `α` where `Zero` is defined, then the block matrix formed by combining `A`, `D`, and zeros is also a diagonal matrix.
|
Matrix.isDiag_iff_diagonal_diag
theorem Matrix.isDiag_iff_diagonal_diag :
∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : DecidableEq n] (A : Matrix n n α),
A.IsDiag ↔ Matrix.diagonal A.diag = A
This theorem, `Matrix.isDiag_iff_diagonal_diag`, states that for any square matrix `A` with entries of type `α` (where `α` has an notion of zero) and indices of type `n` (where `n` has a decidable equality), `A` is a diagonal matrix if and only if `A` is equal to the matrix obtained by setting the diagonal entries of `A` according to the function `A.diag` and setting all other entries to zero. Here, `A.IsDiag` indicates that `A` is a diagonal matrix, and `Matrix.diagonal A.diag` constructs a matrix with the diagonal entries given by `A.diag` and other entries set to zero.
More concisely: A square matrix `A` over a type `α` with decidable equality and indices `n` is diagonal if and only if it is equal to the matrix obtained by setting its diagonal entries to the values in `A.diag` and setting all other entries to zero.
|
Matrix.isDiag_of_subsingleton
theorem Matrix.isDiag_of_subsingleton :
∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : Subsingleton n] (A : Matrix n n α), A.IsDiag
The theorem `Matrix.isDiag_of_subsingleton` states that for any type `α`, and any type `n` that is a subsingleton (i.e., has at most one element), every matrix `A` of type `Matrix n n α` with entries from `α` and indexed by `n` is a diagonal matrix. Here, the `Zero α` instance indicates that `α` has a zero element, and `A.IsDiag` means that `A` is a diagonal matrix, i.e., all entries not on the main diagonal are zero.
More concisely: For any type `α` and subsingleton index type `n`, every `n` x `n` matrix `A` over `α` is a diagonal matrix.
|