Matrix.toLin'_one
theorem Matrix.toLin'_one :
∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
Matrix.toLin' 1 = LinearMap.id
This theorem states that for any commutative semiring `R` and any finite type `n` with decidable equality, the linear transformation corresponding to the identity matrix (denoted as `1` in Lean 4) is the identity linear map. In other words, the matrix-linear map correspondence preserves the notion of identity: just as multiplying by the identity matrix leaves a matrix unchanged, applying the identity linear map leaves a vector unchanged. This theorem thus connects the algebraic concept of identity with its counterpart in linear algebra.
More concisely: For any commutative semiring `R` and finite type `n` with decidable equality, the identity matrix `1` in `R` corresponds to the identity linear map in the matrix-linear map correspondence.
|
Matrix.mulVecLin_mul
theorem Matrix.mulVecLin_mul :
∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : Fintype n]
[inst_2 : Fintype m] (M : Matrix l m R) (N : Matrix m n R), (M * N).mulVecLin = M.mulVecLin ∘ₗ N.mulVecLin
The theorem `Matrix.mulVecLin_mul` states that for any commutative semiring `R` and finite types `l`, `m`, and `n`, given two matrices `M` and `N` with entries in `R`, the multiplication of `M` and `N` followed by applying the linear map `Matrix.mulVecLin` is the same as first applying `Matrix.mulVecLin` to each matrix and then composing the two resulting linear maps. In mathematical terms, it asserts that `(Matrix.mulVecLin (M * N)) = (Matrix.mulVecLin M) ∘ (Matrix.mulVecLin N)`, where `∘` denotes the composition of functions. This theorem is an expression of the associativity property in the context of linear maps and matrix multiplication.
More concisely: For any commutative semiring R and finite types l, m, and n, the composition of the linear maps obtained by multiplying matrices M and N in Lean 4 and applying Matrix.mulVecLin, is equivalent to first applying Matrix.mulVecLin to each matrix and then composing the resulting linear maps.
|
LinearMap.toMatrix_apply
theorem LinearMap.toMatrix_apply :
∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
[inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
[inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Basis n R M₁) (v₂ : Basis m R M₂) (f : M₁ →ₗ[R] M₂) (i : m)
(j : n), (LinearMap.toMatrix v₁ v₂) f i j = (v₂.repr (f (v₁ j))) i
The theorem `LinearMap.toMatrix_apply` states that for any commutative semiring `R`, any types `m` and `n` with finite cardinality, any types `M₁` and `M₂` forming additive commutative monoids and also R-modules, any decidable equality on `n`, any basis `v₁` of `M₁` over `R` indexed by `n`, any basis `v₂` of `M₂` over `R` indexed by `m`, any linear map `f` from `M₁` to `M₂`, and any elements `i` of `m` and `j` of `n`, the `$ij$`-th element of the matrix representation of `f` with respect to the bases `v₁` and `v₂` is the `$i$`-th coordinate of the `v₂`-representation of the image of the `$j$`-th basis vector of `v₁` under `f`.
More concisely: For any commutative semiring R, finite types m and n, additive commutative monoids and R-modules M₁ and M₂, decidable equality on n, bases v₁ of M₁ and v₂ of M₂, linear map f from M₁ to M₂, and i of m and j of n, the ($ij$)th entry of the matrix representation of f with respect to v₁ and v₂ is equal to the i-th coordinate of the image of the j-th basis vector of v₁ under f.
|
Matrix.toLin'_reindex
theorem Matrix.toLin'_reindex :
∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
[inst_1 : DecidableEq n] [inst_2 : Fintype n] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (e₁ : k ≃ m)
(e₂ : l ≃ n) (M : Matrix k l R),
Matrix.toLin' ((Matrix.reindex e₁ e₂) M) =
↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ Matrix.toLin' M ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
The theorem `Matrix.toLin'_reindex` states that for any commutative semiring `R`, types `k`, `l`, `m`, `n`, where `n` and `l` are finite types and have decidable equality, and given equivalences `e₁` from `k` to `m`, `e₂` from `l` to `n`, and a matrix `M` with entries in `R` indexed by `k` and `l`, the linear transformation corresponding to the reindexed matrix `Matrix.reindex e₁ e₂ M` is the same as the linear transformation obtained by first applying the linear equivalence corresponding to the inverse of `e₂`, then the linear transformation corresponding to `M`, and finally the linear equivalence corresponding to the inverse of `e₁`. This theorem expresses a kind of commutativity between matrix reindexing and the corresponding linear transformations.
More concisely: For any commutative semiring `R`, finite types `k`, `l`, `m`, `n` with decidable equality, and equivalences `e₁: k ≤f/" m` and `e₂: l ≤f/" n`, the linear transformation of reindexing `Matrix.reindex e₁ e₂ M` is equivalent to applying the inverse of `e₂`, then `M`, then the inverse of `e₁`.
|
LinearMap.toMatrix_id
theorem LinearMap.toMatrix_id :
∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
{M₁ : Type u_5} [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Basis n R M₁),
(LinearMap.toMatrix v₁ v₁) LinearMap.id = 1
This theorem states that for any commutative semiring `R`, any finite type `n`, any instance of decidable equality on `n`, any additively commutative monoid `M₁`, and any `R`-module structure on `M₁`, if `v₁` is a basis of `M₁` over `R` indexed by `n`, then the matrix representation of the identity linear map with respect to this basis is the identity matrix. In other words, when the identity map is written in terms of basis `v₁`, it corresponds to the identity matrix.
More concisely: For any commutative semiring R, finite type n with decidable equality, additively commutative monoid M₁ with an R-module structure and basis v₁ indexed by n, the identity linear map from M₁ to M₁ with respect to v₁ is represented by the identity matrix.
|
LinearMap.toMatrix_eq_toMatrix'
theorem LinearMap.toMatrix_eq_toMatrix' :
∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
LinearMap.toMatrix (Pi.basisFun R n) (Pi.basisFun R n) = LinearMap.toMatrix'
This theorem states that for any type `R` that forms a commutative semiring, and any type `n` that is finite and has decidable equality, the function `LinearMap.toMatrix` applied to the standard basis `Pi.basisFun R n` is the same as the function `LinearMap.toMatrix'`. In other words, these two ways of converting a linear map to a matrix are equivalent when working with the standard basis in the context of a commutative semiring.
More concisely: For any commutative semiring `R` and finite type `n` with decidable equality, the matrices representing a linear map `LinearMap R` with respect to the standard basis `Pi.basisFun R n` and an arbitrary basis are equal.
|
Matrix.toLin_eq_toLin'
theorem Matrix.toLin_eq_toLin' :
∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
[inst_3 : DecidableEq n], Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'
The theorem `Matrix.toLin_eq_toLin'` states that for any commutative semiring `R` and types `m` and `n` which are finite, and for which `n` has decidable equality, the linear map equivalent to a matrix under the standard basis `Pi.basisFun R n` and `Pi.basisFun R m` (provided by `Matrix.toLin`) is the same as the linear map equivalent to a matrix (provided by `Matrix.toLin'`). Essentially, this theorem links the two different ways of converting a matrix to a linear map, showing that they are equivalent under the conditions specified.
More concisely: For any commutative semiring R and finite types m and n with decidable equality, the linear map represented by a matrix under standard bases of R for m and n, as given by `Matrix.toLin` and `Matrix.toLin'`, are equal.
|
LinearMap.toMatrix'_comp
theorem LinearMap.toMatrix'_comp :
∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
[inst_2 : Fintype n] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (f : (n → R) →ₗ[R] m → R)
(g : (l → R) →ₗ[R] n → R), LinearMap.toMatrix' (f ∘ₗ g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
This theorem states that for any commutative semiring `R` and types `l`, `m`, `n` with `n` and `l` being finite and having decidable equality, the composition of two linear maps `f : (n → R) →ₗ[R] m → R` and `g : (l → R) →ₗ[R] n → R` can be expressed in terms of the matrix representation of the individual maps. Specifically, the matrix representation of the composition of `f` and `g` is equal to the product of the matrix representation of `f` and the matrix representation of `g`. This result is a reflection of the associativity property in linear algebra, where the composition of two linear transformations corresponds to the product of their matrix representations.
More concisely: Given commutative semirings `R`, finite types `l`, `m`, `n` with decidable equality, the matrix representation of the composition of linear maps `f : (n → R) →ₗ[R] m` and `g : (l → R) →ₗ[R] n` equals the product of the matrix representations of `f` and `g`.
|
Matrix.toLin'_mul_apply
theorem Matrix.toLin'_mul_apply :
∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
[inst_2 : Fintype n] [inst_3 : Fintype m] [inst_4 : DecidableEq m] (M : Matrix l m R) (N : Matrix m n R)
(x : n → R), (Matrix.toLin' (M * N)) x = (Matrix.toLin' M) ((Matrix.toLin' N) x)
This theorem, `Matrix.toLin'_mul_apply`, is a shortcut lemma combining `Matrix.toLin'_mul` and `LinearMap.comp_apply`. Given a commutative semiring `R`, types `l`, `m`, and `n`, and matrices `M` of type `Matrix l m R` and `N` of type `Matrix m n R`, and a vector `x` of type `n → R` (a function from `n` to `R`), the linear map from `n` to `R` obtained by applying `Matrix.toLin'` to the product `M * N` and then applying this linear map to `x` is the same as first applying `Matrix.toLin'` to `N` and `x`, then applying `Matrix.toLin'` to `M` and the result of the first application. Note that `DecidableEq n`, `Fintype n`, `Fintype m`, and `DecidableEq m` are required, meaning that equality is decidable and the types `n` and `m` must be finite.
More concisely: Given commutative semirings `R`, finite types `n`, `m`, matrices `M` of size `m x n` and `N` of size `n x r` over `R`, and a vector `x : n → R`, the linear map obtained by composing `Matrix.toLin' M` with `Matrix.toLin' (M * N)` and then applying it to `x` is equal to the linear map obtained by applying `Matrix.toLin' N` to `x`, then applying `Matrix.toLin' M` to the resulting vector.
|
Matrix.mulVecLin_reindex
theorem Matrix.mulVecLin_reindex :
∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
[inst_1 : Fintype n] [inst_2 : Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R),
((Matrix.reindex e₁ e₂) M).mulVecLin =
↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
The theorem `Matrix.mulVecLin_reindex` states that for any commutative semiring `R`, types `k`, `l`, `m`, `n` where `n` and `l` are finite types, and equivalences `e₁` from `k` to `m` and `e₂` from `l` to `n`, and a matrix `M` with entries in `R` indexed by `k` and `l`, the linear multiplication of a reindexed matrix `M` (reindexed from `k` by `l` to `m` by `n`) is equal to the composition of the linear congruence on `R` reindexed by `e₁` in reverse, the linear multiplication of matrix `M`, and the linear congruence on `R` reindexed by `e₂`. This essentially says that reindexing a matrix and then performing a linear multiplication is the same as first performing the linear multiplication and then reindexing.
More concisely: For any commutative semiring `R`, finite types `k`, `l`, `m`, `n`, equivalences `e₁ : k ≃ m` and `e₂ : l ≃ n`, and a matrix `M` over `R` indexed by `k` and `l`, the linear multiplication of the reindexed matrix `M` is equal to the composition of the reindexed linear congruences and the linear multiplication of `M`.
|
Matrix.toLin'_mul
theorem Matrix.toLin'_mul :
∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
[inst_2 : Fintype n] [inst_3 : Fintype m] [inst_4 : DecidableEq m] (M : Matrix l m R) (N : Matrix m n R),
Matrix.toLin' (M * N) = Matrix.toLin' M ∘ₗ Matrix.toLin' N
The theorem `Matrix.toLin'_mul` states that for every commutative semiring `R`, types `l`, `m`, and `n`, where `m` and `n` are finite types with decidable equality, and for every two matrices `M` and `N` with entries in `R` (where `M` has rows indexed by `l` and columns indexed by `m`, and `N` has rows indexed by `m` and columns indexed by `n`), the linear map equivalent to the matrix multiplication of `M` and `N` is equal to the composition of the linear map equivalents of `M` and `N`.
In mathematical terms, if we consider matrices as linear maps, then the multiplication of two matrices corresponds to the composition of the two corresponding linear maps.
More concisely: For every commutative semiring R and finite types l, m, n with decidable equality, the matrix multiplication of two matrices M and N with entries in R, where M has dimensions l x m and N has dimensions m x n, is equal to the composition of the linear maps represented by M and N.
|
LinearMap.toMatrix'_id
theorem LinearMap.toMatrix'_id :
∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
LinearMap.toMatrix' LinearMap.id = 1
The theorem `LinearMap.toMatrix'_id` states that for any commutative semiring `R` and any type `n` with decidable equality and finiteness, when the identity linear map (which maps each element to itself) is converted to a matrix using the `LinearMap.toMatrix'` function, the resulting matrix is the identity matrix (each diagonal element is 1 and off-diagonal elements are 0). This means that the matrix representation of the identity linear map is indeed the identity matrix, which is consistent with linear algebra theory.
More concisely: For any commutative semiring R and type n with decidable equality and finiteness, the matrix representation of the identity linear map is the identity matrix.
|