Matrix.mulVecᵣ_eq
theorem Matrix.mulVecᵣ_eq :
∀ {l m : ℕ} {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α),
A.mulVecᵣ v = A.mulVec v
This theorem, named `Matrix.mulVecᵣ_eq`, states that for any natural numbers `l` and `m`, and any type `α` that forms a non-unital, non-associative semiring, given a matrix `A` with `l` rows and `m` columns, and a vector `v` of length `m`, both with entries in `α`, the result of multiplying `A` by `v` using the `mulVecᵣ` operation is equal to the result of using the `mulVec` operation. This theorem can be used to prove that the product of a 2x2 matrix `A` with entries `a₁₁`, `a₁₂`, `a₂₁`, `a₂₂` and a 2-dimensional vector `v` with entries `b₁`, `b₂` is the vector with entries `a₁₁*b₁ + a₁₂*b₂` and `a₂₁*b₁ + a₂₂*b₂`.
More concisely: For any non-unital, non-associative semiring type `α`, matrix `A` of size `l x m` over `α`, and vector `v` of length `m` over `α`, `A · v = MulVec A v` holds.
|
Matrix.vecMulᵣ_eq
theorem Matrix.vecMulᵣ_eq :
∀ {l m : ℕ} {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α),
Matrix.vecMulᵣ v A = Matrix.vecMul v A
The theorem `Matrix.vecMulᵣ_eq` states that for any natural numbers `l` and `m`, and for any type `α` that forms a non-unital, non-associative semiring, the custom-defined right vector-matrix multiplication `Matrix.vecMulᵥ` is equivalent to the standard vector-matrix multiplication `Matrix.vecMul`. In more specific terms, given a vector `v` of length `l` with entries from `α`, and a `l` by `m` matrix `A` with entries from `α`, the result of right-multiplying the vector `v` by the matrix `A` using our custom-defined multiplication is the same as using the standard multiplication. This theorem can be used to prove that the multiplication of a 2-element vector by a 2x2 matrix gives a 2-element result vector with its elements calculated by a specified formula.
More concisely: For any non-unital, non-associative semiring type `α`, the custom-defined right vector-matrix multiplication `Matrix.vecMulᵣ` equals the standard vector-matrix multiplication `Matrix.vecMul` for vectors and matrices of compatible sizes.
|
Matrix.forall_iff
theorem Matrix.forall_iff :
∀ {α : Type u_1} {m n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop),
Matrix.Forall P ↔ ∀ (x : Matrix (Fin m) (Fin n) α), P x
The theorem `Matrix.forall_iff` provides a characterization of a property holding for all matrices over a given type. Specifically, for any type `α` and natural numbers `m` and `n`, it states that a property `P` holds for all matrices of size `m` by `n` with entries in `α` if and only if `P` holds for every possible matrix `x`, where `x` is a matrix of size `m` by `n` with entries in `α`. In other words, it establishes the equivalence between the universal quantification of a property over all matrices and the universal quantification of the same property over all possible entries of such matrices.
More concisely: For any type `α`, property `P`, natural numbers `m` and `n`, the statement "for all matrices X of size `m` by `n` over `α`, `P(X)` holds" is equivalent to "for all matrices `x` of size `m` by `n` with entries in `α`, `P(x)` holds".
|
Matrix.exists_iff
theorem Matrix.exists_iff :
∀ {α : Type u_1} {m n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop), Matrix.Exists P ↔ ∃ x, P x
This theorem states that for any types `α`, natural numbers `m` and `n`, and a property `P` that takes a matrix with `m` rows and `n` columns with elements of type `α`, there exists a matrix that satisfies the property `P` if and only if there exists an element `x` such that the property `P` holds when applied to `x`. This theorem can be used to prove that the existence of matrices satisfying a given property can be expressed in terms of the existence of individual elements satisfying that property.
More concisely: For any type `α`, property `P` on `m x n` matrices over `α`, and natural numbers `m` and `n`, the property `P` has a solution if and only if there exists an `α` element `x` such that `P` holds on the matrix constructed from `x` repeated `m` times in rows.
|
Matrix.dotProductᵣ_eq
theorem Matrix.dotProductᵣ_eq :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : AddCommMonoid α] {m : ℕ} (a b : Fin m → α),
Matrix.dotProductᵣ a b = Matrix.dotProduct a b
The theorem `Matrix.dotProductᵣ_eq` states that for any type `α` that has multiplication and addition, any natural number `m`, and any two functions `a` and `b` from `Fin m` to `α`, the alternative version of matrix dot product (`Matrix.dotProductᵣ`) produces the same result as the standard matrix dot product (`Matrix.dotProduct`). In other words, for the given vectors `a` and `b`, the sum of the entrywise products using `Matrix.dotProductᵣ` and `Matrix.dotProduct` are equal. This theorem would be used, for instance, to prove that the dot product of two 2-dimensional vectors `[a, b]` and `[c, d]` is `a * c + b * d`.
More concisely: For any type `α` with multiplication and addition, and for any functions `a : Fin m → α` and `b : Fin n → α`, the entrywise matrix dot product `Matrix.dotProductᵣ a b` equals the standard matrix dot product `Matrix.dotProduct a.toMatrix b.toMatrix`.
|
Matrix.transposeᵣ_eq
theorem Matrix.transposeᵣ_eq : ∀ {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α), A.transposeᵣ = A.transpose
This theorem, `Matrix.transposeᵣ_eq`, establishes the equality between two transpose operations on a matrix with entries in arbitrary type `α`. This matrix's rows and columns are indexed by finite sets of size `m` and `n` respectively. The theorem states that for any such matrix `A`, the operation `transposeᵣ` applied to `A` is equivalent to simply transposing `A`. In other words, for all matrices `A` of the specified type, `A.transposeᵣ = A.transpose`. This can be used, for example, to prove that the transpose of a 2x2 matrix `!![a, b; c, d]` is `!![a, c; b, d]`.
More concisely: For any matrix of size `m` by `n` with entries in arbitrary type `α`, the transpose operation `.transposeᵣ` is equal to the standard matrix transpose.
|
Matrix.mulᵣ_eq
theorem Matrix.mulᵣ_eq :
∀ {l m n : ℕ} {α : Type u_1} [inst : Mul α] [inst_1 : AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α)
(B : Matrix (Fin m) (Fin n) α), A.mulᵣ B = A * B
This theorem, `Matrix.mulᵣ_eq`, states that for any natural numbers `l`, `m`, and `n`, and any type `α` that is a multiplicative and additive commutative monoid, the right multiplication operation `mulᵣ` on any two matrices `A` and `B` of suitable dimensions is equal to their standard matrix multiplication `*`. Specifically, if `A` is an `l`-by-`m` matrix and `B` is an `m`-by-`n` matrix (with entries in `α`), then `A.mulᵣ B = A * B`. The theorem essentially formalizes one of the fundamental properties of matrix multiplication in the context of lean 4.
More concisely: For any natural numbers `l`, `m`, and `n`, and any commutative monoid `α`, the right multiplication of an `l`-by-`m` matrix `A` with an `m`-by-`n` matrix `B` over `α` is equal to their standard matrix multiplication.
|
Matrix.etaExpand_eq
theorem Matrix.etaExpand_eq : ∀ {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α), A.etaExpand = A
The theorem `Matrix.etaExpand_eq` establishes that for any matrix `A` with entries in some type `α` and dimensions `m` and `n`, the operation `etaExpand` applied on `A` is equal to `A` itself. In other words, for any matrix `A` of type `Matrix (Fin m) (Fin n) α`, the expression `A.etaExpand` is equivalent to `A`. This effectively means that `etaExpand` is an identity operation on the matrix `A`. The theorem can be used to prove that a matrix is equal to a list of its elements arranged in its original row and column order.
More concisely: For any matrix `A` of type `Matrix (Fin m) (Fin n) α` in Lean 4, the operation `etaExpand A` equals the matrix `A` itself.
|