Linear Algebra Rosetta Stone

• Definition 1.1 (complex numbers, \(\mathbb{C}\))
  • A Complex Number is an ordered pair \((a,b)\) where \(a,b\in\mathbb{R}\). We write this as \(a + \mathrm{i}b\).
    • In Mizar, instead of working with the Cartesian product \(\mathbb{R}\times\mathbb{R}\), we use the product of an indexed family with two members \(X_{0}=\mathbb{R}\) and \(X_{1}=\mathbb{R}\). This is equivalent to the set \(z\in\hom(\{0,1\},\mathbb{R})\iff z\in\prod_{\alpha=0,1}X_{\alpha}\) and this is precisely how Mizar defines complex numbers.
    • Since this is kind of confusing, there is also the notation [*a,b*] for the complex number \(a+\mathrm{i}b\) which is defined in ARYTM_0:def 5.
    • Note that Mizar follows mathematical practice, and sets \(\mathbb{C}=\{(a,b)\in\mathbb{R}^{2}\mid b\neq0\}\cup\mathbb{R}\) so that \(\mathbb{R}\subset\mathbb{C}\) is true.
  • The set of all complex numbers is denoted by \(\mathbb{C} = \{a+\mathrm{i}b\mid a,b\in\mathbb{R}\}\).
    • In Mizar, this is denoted COMPLEX (and defined in NUMBERS:def 2)
  • Addition and multiplication in \(\mathbb{C}\) are defined as: \((a + \mathrm{i}b)+(c+\mathrm{i}d) = (a+c)+\mathrm{i}(b+d)\) \((a + \mathrm{i}b)(c+\mathrm{i}d) = (ac-bd)+\mathrm{i}(ad+bc)\)
    • XCMPLX_0:def 3 defines addition of complex numbers
    • XCMPLX_0:def 4 defines multiplication of complex numbers
• The choice of \(\mathrm{i}=(0,1)\) is due to Euler, and it is encoded in Mizar as <i> as defined in XCMPLEX_0:def 1
• Theorem 1.3. Properties of Complex Arithmetic
  • Addition and multiplication are both commutative
    • This is built into the definition
  • Addition is associative (XCMPLX_1:1)
  • Multiplication is associative (XCMPLX_1:4)
  • 0 is the additive identity & 1 is the multiplicative identity (this is true thanks to using the real numbers)
  • Every \(\alpha\in\mathbb{C}\) has a unique \(\beta\in\mathbb{C}\) such that \(\alpha+\beta=0\)
    • This is negation, and defined in XCMPLX_0:def 5
  • Every \(\alpha\in\mathbb{C}\) has a unique \(\beta\in\mathbb{C}\) such that \(\alpha\beta=1\)
    • This is inversion and defined in XCMPLX_0:def 6
  • Distributivity \(\lambda(\alpha+\beta)=\lambda\alpha + \lambda\beta\) for every \(\alpha,\beta,\lambda\in\mathbb{C}\)
• Definition 1.5.
  • Subtraction is defined as \(\alpha-\beta=\alpha+(-\beta)\) (XCMPLX_0:def 7)
  • Division is defined as multiplying by the inverse of the denominator \(\alpha/\beta=\alpha\cdot\beta^{-1}\) (XCMPLX_0:def 8)
• Convention: throughout the book, \(\mathbb{F}\) to stand for either \(\mathbb{R}\) or \(\mathbb{C}\).

• Aside: Mathematicians informally talk about lists and \(n\) tuples. This is formalized in Mizar using finite sequences in the FINSEQ series of articles.
• Definition 1.8.
  • Let \(n\) be a non-negative integer. A List of length \(n\) is an ordered collection of \(n\) elements.
    • This is precisely formalized as a FinSequence in Mizar, which is a function whose domain is \(\{1,2,\dots,n\}\)
    • We can also use the Mizar definition n-tuples_on F to refer to the set of all \(n\) tuples (i.e., FinSequence of length \(n\)) with entries in \(F\)
  • Two lists are equal if and only if they have the same elements in the same order.
    • This is precisely FINSEQ_1:def 17

• Definition 1.11.
  • \(\mathbb{F}^{n}\) denotes the set of all lists of length \(n\) of elements of \(\mathbb{F}\)
    • In Mizar, this could be formalized as Funcs(Seg n,COMPLEX) or Funcs(Seg n,REAL)
  • If \((x_{1},\dots,x_{n})\in\mathbb{F}^{n}\) and \(k\in\{1,\dots,n\}\), then \(x_{k}\) is the \(k^{\text{th}}\) coordinate of \(x\).
    • In Mizar, this is denoted x.k
• Definition 1.13. Addition in \(\mathbb{F}^{n}\) is defined componentwise \((x_{1},\dots,x_{n})+(y_{1},\dots,y_{n})=(x_{1}+y_{1},\dots,x_{n}+y_{n})\).
  • This is formalized in FVSUM_1:def 3.
• Theorem 1.14 (Commutativity of addition in \(\mathbb{F}^{n}\)). If \(x,y\in\mathbb{F}^{n}\), then \(x+y=y+x\).
  • This is automatic with the registrations of FVSUM_1
• Notation 1.15 (0). It's common to denote by 0 the list of length \(n\) whose entries are all zero.
  • In Mizar, we can denote this by (n |-> 0) using FINSEQ_2:def 2
• Definition 1.17 (Additive inverse on \(\mathbb{F}^{n}\)). For \(x\in\mathbb{F}^{n}\), the Additive Inverse of \(x\), denoted \(-x\), is the element \(-x\in\mathbb{F}^{n}\) such that \(x+(-x)=0\).
  • This is definition FVSUM_1:def 4
• Definition 1.18 (Scalar multiplication on \(\mathbb{F}^{n}\)). The Product of a number \(\lambda\in\mathbb{F}\) and a vector \(x=(x_{1},\dots,x_{n})\in\mathbb{F}^{n}\) is the vector obtained by multiplying componentwise by \(\lambda\): \(\lambda x=(\lambda x_{1},\dots,\lambda x_{n})\).
  • This is definition FVSUM_1:def 6

Axler gives a brief digression about fields. I will take this opportunity to discuss Mizar's formalization Field of fields.

Introductory linear algebra courses give the uninspiring definition of a field as something along the lines of:

• Implicit Definition. A Field consists of a set \(\mathbb{F}\) equipped with

  • addition \(+\colon\mathbb{F}\times\mathbb{F}\to\mathbb{F}\)
  • negation \(-\colon\mathbb{F}\to\mathbb{F}\)
  • a constant \(0\in\mathbb{F}\)
  • multiplication \(\,\cdot\,\colon\mathbb{F}\times\mathbb{F}\to\mathbb{F}\)
  • inversion \((-)^{-1}\colon\mathbb{F}\to\mathbb{F}\) (Mizar denoted \(x^{-1}\) as x")
  • a constant \(1\in\mathbb{F}\)

  such that

  • addition is commutative \(x+y=y+x\) (Abelian)
  • addition is associative \(x+(y+z)=(x+y)+z\) (add-associative)
  • zero is unit for addition: \(x+0=x\) (right_zeroed) and as a consequence of commutativity \(0+x=x\)
  • negation gives additive inverse \(x+(-x)=0\) (right_complementable)
  • multiplication is commutative \(xy=yx\) (commutative)
  • multiplication is associative \((xy)z=x(yz)\) (associative)
  • one is the unit for multiplication \(1\cdot x=x\cdot 1=x\) (well-unital)
  • inversion is the multiplicative inverse when \(x\neq0\), \(x^{-1}\cdot x=1\) (almost_left_invertible = all nonzero elements are left_invertible) and then commutativity gives us \(x\cdot x^{-1}=1\)
  • multiplication distributes over addition: \(x(y+z)=xy+xz\) (distributive)

Later on, students learn there is a hierarchy of generalizations of fields (rings and things).

Idiomatic Mizar defines a structure, then attaches adjectives to it to form a mathematical gadget. The underlying structure for fields coincides with rings (and things), and is formalize as doubleLoopStr in Mizar.

The bare minimum we need to formalize the notion of a field requires:

• a set \(F\)
• a function \(+\colon F\times F\to F\) (addF in Mizar)
• a function \(\cdot F\times F\to F\) (multF in Mizar)
• a constant \(1_{F}\in F\) (OneF in Mizar)
• another constant \(0_{F}\in F\) (ZeroF in Mizar).

There are utility functions like 0.F to refer to the ZeroF of F, and 1.F for the OneF of F.

Mizar then uses adjectives to define:

• a Ring is a nonempty double loop satisfying all the properties of a field except (1) the commutativity of multiplication and (2) almost left invertibility (i.e., every nonzero element of the field has a multiplicative inverse)
• a Skew-Field is a nondegenerated (i.e., \(0\neq 1\)) almost left invertible Ring
• a Field is a commutative Skew-Field

If we want to consider the real numbers as a field, we would use F_Real.

If we want to consider the complex numbers as a field, we would use F_Complex.

• Definition 1.36. Suppose \(V_{1}\), …, \(V_{m}\) are subspaces of \(V\). We define the Sum of \(V_{1}\), …, \(V_{m}\) (denoted by \(V_{1}+ \dots + V_{m}\)) to be the set \(V_{1}+ \dots + V_{m} = \{v_{1} + \dots + v_{m}\mid v_{1}\in V_{1},\dots,v_{m}\in V_{m}\}\).
  • VECTSP_5:def 1
• Implicit Theorem. We have for any subspaces \(V_{1}\) and \(V_{2}\) of \(V\), \(V_{1}+V_{2} = V_{2}+V_{1}\). (VECTSP_5:5)
• Implicit Theorem. For any subspaces \(V_{1}\), \(V_{2}\), \(V_{3}\) of \(V\), we have \(V_{1}+(V_{2}+V_{3})=(V_{1}+V_{2})+V_{3}\). (VECTSP_5:6).
• Implicit Theorem. For any subspaces \(V_{1}\) and \(V_{2}\) of \(V\), \(V_{1}\) is a subspace of \(V_{1}+V_{2}\) and \(V_{2}\) is a subspace of \(V_{1}+V_{2}\). (VECTSP_5:7)

• Definition 1.41. Let \(V_{1}\), …, \(V_{m}\) be subspaces of \(V\). The sum \(V_{1} + \dots + V_{m}\) is called a Direct Sum if each element of the sum can be written in only one way as a sum, and in that case we write \(V_{1}\oplus\dots\oplus V_{m}\).
  • VECTSP_5:def 4 defines M is_the_direct_sum_of V1,V2 as a predicate
  • Theorems VECTSP_5:48 and VECTSP_5:49 prove the logical equivalence of this definition and Mizar's definition.
• Theorem 1.45 (Conditions for a direct sum). Let \(V_{1}\), …, \(V_{m}\) be subspaces of \(V\). Then \(V_{1} + \dots + V_{m}\) is a direct sum if and only if the only way to write \(0\) as a sum \(v_{1}+\dots+v_{m}\) (with \(v_{1}\in V_{1}\), …, \(v_{m}\in V_{m}\)) is by taking each \(v_{k}=0\).
  • Missing from Mizar but this can be easily deduced as a consequence from other results.
• Theorem 1.46 (Direct sum of two subspaces). Suppose \(U\) and \(W\) are subspaces of \(V\). Then \(U+W\) is a direct sum if and only if \(U\cap W=\{0\}\).
  • This is taken as the definition VECTSP_5:def 4
• Implicit Theorem. If \(V_{1}=V_{2}\oplus V_{3}\), then \(V_{1}=V_{3}\oplus V_{2}\). (VECTSP_5:41)

• Definition 2.2. Let \(v_{1}\), …, \(v_{m}\) be vectors in \(V\). A Linear Combination of \(v_{1}\), …, \(v_{m}\) is any vector of the form \(a_{1}v_{1}+\dots+a_{m}v_{m}\) where \(a_{1},\dots,a_{m}\in\mathbb{F}\).
  • Mizar appears to define the coefficients \(a_{1}\), …, \(a_{m}\) for a particular linear combination as LinearCombination of A where \(A=\{v_{1},\dots,v_{m}\}\). See Theorem VECTSP_6:18 for example.
• Definition 2.4. The set of all linear combinations of a list of vectors \(v_{1}\), …, \(v_{m}\) of \(V\) is called the Span of \(v_{1}\), …, \(v_{m}\) and is denoted by \(\operatorname{span}(v_{1},\dots,v_{m})=\{a_{1}v_{1}+\dots+a_{m}v_{m}\mid a_{1},\dots,a_{m}\in\mathbb{F}\}\).
  • VECTSP_7:def 2 calls it Lin
• Definition 2.9. A vector space is called Finite-Dimensional if some finite list of vectors in it spans the space.
  • MATRLIN:def 1 uses an equivalent condition, namely, that there is a finite linearly independent subset which spans the space.
• Definition 2.13. A vector space is called Infinite-DImensional if it is not finite-dimensional. Missing from Mizar

• Definition 2.15. A list of vectors \(v_{1}\), …, \(v_{m}\) of \(V\) is called Linearly Independent if the only choice of coefficients \(a_{1},\dots,a_{m}\in\mathbb{F}\) which satisfies \(0 = a_{1}v_{1} + \dots + a_{m}v_{m}\) is \(a_{1}=\dots=a_{m}=0\).
  • VECTSP_7:def 1 formalizes linearly-independent for a set of vectors.
  • \(\emptyset\) is registered as linearly independent in VECTSP_7
• Definition 2.17. A list of vectors is called Linearly Dependent if it is not linearly independent.
• Theorem 2.19 (Linear dependence lemma). Let \(v_{1}\), …, \(v_{m}\) be linearly dependent in \(V\). Then there exists a \(k\in\{1,\dots,m\}\) such that \(v_{k}\in\operatorname{span}(v_{1},\dots,v_{k-1})\). Further, if \(k\) satisfies the condition above, then \(\operatorname{span}(v_{1},\dots,v_{k-1},v_{k+1},\dots,v_{m})=\operatorname{span}(v_{1},\dots,v_{m})\).
  • Missing from Mizar but I suspect it can be deduced from VECTSP_9:14
• Theorem 2.22. In finite-dimensional vcetor spaces, the length of every linearly independent list of vectors is less than or equal to the length of every spanning set of vectors.
  • This seems to be deducible from VECTSP_7:19 but is Missing from Mizar
• Theorem 2.25 (finite-dimensional subspaces). Every subspace of a finite-dimensional vector space is finite-dimension. (VECTSP_9:24)

• Definition 3.1. Let \(V\), \(W\) be vector spaces over the same field \(\mathbb{F}\). A Linear Map from \(V\) to \(W\) is a function \(T\colon V\to W\) such that it is:
  • Additive: \(T(u+v)=T(u)+T(v)\) for all \(u,v\in V\) (additive)
  • Homogeneous: \(T(\lambda v)=\lambda T(v)\) for all \(\lambda\in\mathbb{F}\) and \(v\in V\) (homogeneous)
  • RANKNULL defines linear-transformation of V,W as an additive homogeneous Function of V,W.
• Notation 3.2. Let \(V\), \(W\) be vector spaces over \(\mathbb{F}\)
  1. The set of linear maps from \(V\) to \(W\) is denoted \(\mathcal{L}(V,W)\)
  2. The set of linear maps from \(V\) to \(V\) is denoted \(\mathcal{L}(V)=\mathcal{L}(V,V)\)
• Examples 3.3.
  1. The zero map \(V\to W\) sending every vector to the zero vector of \(W\) is linear. Missing from Mizar
  2. The identity operator \(\id\colon V\to V\) is linear. Missing from Mizar
• Theorem 3.4. Suppose \(v_{1}\), …, \(v_{n}\) is a basis for \(V\) and \(w_{1}\), …, \(w_{n}\) is a basis for \(W\). Then there exists a linear transformation \(T\colon V\to W\) such that \(T(v_{i})=w_{i}\) for each \(i=1,\dots,n\). Missing from Mizar

• Definition 3.5. Suppose \(S\), \(T\in\mathcal{L}(V,W)\). Then we define their sum \(S+T\) to be the linear transformation defined by \((S+T)(v)=S(v)+T(v)\) for every \(v\in V\). (MATRLIN:def 3)

  When \(\lambda\in\mathbb{F}\), we define the product \(\lambda S\) as the linear transformation defined by \((\lambda S)(v)=\lambda\cdot S(v)\) for every \(v\in V\). (MATRLIN:def 4)

• Theorem 3.6. With these operations we just defined, \(\mathcal{L}(V,W)\) forms a vector space over \(\mathbb{F}\).
• Definition 3.7. Let \(S\in\mathcal{U,W}\), \(T\in\mathcal{L}(V,U)\). We define the Composition of linear operators \(S\circ T\) to be defined as \((S\circ T)(v)=S(T(v))\) for every \(v\in V\).
  • This is handled for free using composition of functions in Mizar. Composition is originally defined for arbitrary relations in RELAT_1:def 8.
  • MATRLIN2 explicitly coerces the types
• Theorem 3.8.
  • Associativity: \((T_{1}\circ T_{2})\circ T_{3}=T_{1}\circ (T_{2}\circ T_{3})\) (RELAT_1:36)
  • Identity: \(T\circ I=I\circ T=T\) (FUNCT_2:17)
  • \((S_{1}+S_{2})\circ T=(S_{1}\circ T) + (S_{2}\circ T)\) Missing from Mizar
• Theorem 3.10. Let \(T\colon V\to W\) be a linear transformation. Then \(T(0)=0\). (RANKNULL:9)

• Definition 3.11. Let \(T\in\mathcal{L}(V,W)\) be a linear transformation. We define the Null Space of \(T\) (or, the "kernel" of \(T\)) denoted \(\operatorname{null}(T)\) or \(\ker(T)\), is the subset of \(V\) consisting of vectors which \(T\) maps to \(0\), i.e., \(\ker(T)=\{v\in V\mid T(v)=0\}\). (RANKNULL:def 1)
• Theorem 3.13. The null space is actually a subspace. (Mizar noted this in its definition.)
• Definition 3.14. A function \(T\colon V\to W\) is called Injective (or "one-to-one") if \(T(u)=T(v)\) implies \(u=v\) for any \(u,v\in V\). (FUNCT_1:def 4)
• Theorem 3.15 (Injectivity \(\iff\) null space equals \(\{0\}\)). Let \(T\in\mathcal{L}(V,W)\) be a linear transformation. Then \(T\) is injective if and only if \(\ker(T)=\{0\}\).
  • The forward direction is proven in (RANKNULL:15)
  • The backward direction is obvious as a consequence of the rank-null theorem, but explicitly stated is Missing from Mizar

• Definition 3.16. Let \(T\in\mathcal{L}(V,W)\) be a linear transformation. The Range of \(T\) is the subset \(W\) consisting of the elements that are equal to \(T(v)\) for some \(v\in V\); i.e., \(\operatorname{range}(T)=\{T(v)\mid v\in V\}\).
  • This is also known as the Image of \(T\) and is defined in RANKNULL:def 2.
• Theorem 3.18. If \(T\in\mathcal{L}(V,W)\), then \(\operatorname{range}(T)\) is a subspace of \(W\). (This is handled already in the definition in Mizar.)
• Definition 3.19. A function \(f\colon X\to Y\) is called Surjective (or Onto) if its range is equal to \(W\). (FUNCT_2:def 3)

• Theorem 3.21 (Fundamental theorem of linear maps). Suppose \(V\) is finite-dimensional vector space, and let \(T\in\mathcal{L}(V,W)\). Then the range is finite-dimensional and \(\dim(V)=\dim\ker(T)+\dim\operatorname{range}(T)\).
  • The \(\dim\ker(T)\) is called the Nullity of \(T\) and the \(\dim\operatorname{range}(T)\) is called the Rank of \(T\)
  • (RANKNULL:44) proves this theorem
  • (MATRLIN2:43) proves both directions of this theorem for vector spaces over fields
• Theorem 3.22. Suppose \(V\) and \(W\) are finite-dimensional vector spaces over \(\mathbb{F}\). If \(\dim(V)\gt\dim(W)\), then there is no linear map from \(V\) to \(W\) that is injective.
  • Missing from Mizar But it can be proven quickly from RANKNULL:45
• Theorem 3.24. Suppose \(V\) and \(W\) are finite-dimensional vector spaces over \(\mathbb{F}\). If \(\dim(V)\lt\dim(W)\), then there is no linear map from \(V\) to \(W\) that is surjective. Missing from Mizar
• Theorem 3.26. A homogeneous system of linear equations with more variables than equations has nonzero solutions. Missing from Mizar
• Theorem 3.28. An inhomogeneous system of linear equations with more equations than variables has no solution for some choice of the constant terms. Missing from Mizar

• Definition 3.29. Suppose \(m\) and \(n\) are nonnegative integers natural numbers. A m-by-n Matrix \(A\) is an array of elements of \(\mathbb{F}\) with \(m\) rows and \(n\) columns. The notation \(A_{j,k}\) refers to the entry in row \(j\) and column \(k\) of \(A\).
  • MATRIX_0 defines Matrix of m,n,D for entries in a non-empty set \(D\)
  • The n is encoded as the width M for an m-by-n matrix \(M\)
  • The m is encoded as len (dom M) for an m-by-n matrix \(M\)
  • MATRIX_0:def 4 encodes the possible index pairs for a matrix as Index M
  • \(A_{i,j}\) is encoded in Mizar as A * (i,j) (MATRIX_0:def 5)
• Implicit notion. Let \(A\) and \(B\) are both m-by-n matrices. If \(A_{i,j}=B_{i,j}\) for every \(i\) and \(j\), then \(A=M\) (MATRIX_0:21)
• Definition 3.31 (Matrix of a Linear Map). Let \(T\in\mathcal{L}(V,W)\) be a linear transformation, let \(v_{1}\), …, \(v_{m}\) be a basis of \(V\) and \(w_{1}\), …, \(w_{n}\) be a basis for \(W\). The Matrix of \(T\) with respect to these bases is the m-by-n matrix whose entries \(A_{i,j}\) are defined by: \(T(v_{k})=A_{1,k}w_{1} + \dots + A_{m,k}w_{k}\). This is denoted \(\mathcal{M}(T)\) for the matrix.
  • MATRLIN2 redefines AutMt to give the associated matrix for a linear operator
  • MATRLIN2:def 2 defines AutEqMt for linear operators
• Implicit Example. The identity linear transformation corresponds to the identity matrix. (MATRLIN2:28)
• Implicit Definition. For any matrix of suitable dimension, we can find a linear transformation between vector spaces of suitable dimensions. This is the inverse operation of finding the matrix associated to a linear transformation and particular choice of bases.
  • MATRLIN2:def 3 defines this as Mx2Tran

• Definition 3.34. The Sum of two matrices of the same size is the matrix obtained by componentwise addition.
• Theorem 3.35. Suppose \(S,T\in\mathcal{L}(V,W)\). Then \(\mathcal{M}(S+T)=\mathcal{M}(S)+\mathcal{M}(T)\).
  • In this form, it is MATRLIN:42 and the inverse operation is proven in MATRLIN2:37
• Definition 3.36 (Scalar multiplication of matrices). We can define scalar multiplication of a matrix by simply multiplying every component by (the same) scalar. (MATRIX_3:def 5)
• Theorem 3.38. Let \(\lambda\in\mathbb{F}\) and \(T\in\mathcal{L}(V,W)\). Then \(\mathcal{M}(\lambda T) =\lambda \mathcal{M}(T)\). (MATRLIN:43)
• Notation 3.39. For positive integers \(m\) and \(n\), we denote the set of all m-by-n matrices with entries in \(\mathbb{F}\) by \(\mathbb{F}^{m,n}\).
  • Mizar calls the set of square n-by-n matrices as n-Matrices_over K (MATRIX_1:def 1)
• Theorem 3.40. For positive integers \(m\) and \(n\), the collection \(\mathbb{F}^{m,n}\) with matrix addition and scalar multiplication forms a finite-dimensional vector space over \(\mathbb{F}\) of dimension \(mn\). Missing from Mizar

• Definition 3.41 (Matrix multiplication). Let \(A\) be an m-by-n matrix and \(B\) is an n-by-p matrix. The Product \(AB\) is the m-by-p matrix whose components are given by \((AB)_{i,k} = \sum_{j}A_{i,j}B_{j,k}\). (MATRIX_3:def 4)
• Theorem 3.43. Let \(T\in\mathcal{L}(U,V)\) and \(S\in\mathcal{L}(V,W)\), then \(\mathcal{M}(S\circ T)=\mathcal{M}(S)\mathcal{S}(T)\).
  • I think this is MATRLIN:41, but I might be mistaken…

• Definition 3.59.
  1. A linear map \(T\in\mathcal{L}(V,W)\) is called Invertible if there exists a \(S\in\mathcal{L}(W,V)\) such that \(S\circ T\) is the identity operator on \(V\) and \(T\circ S\) is the identity operation on \(W\). Missing from Mizar
  2. A linear map \(S\in\mathcal{L}(W,V)\) satisfying \(T\circ S = I\) and \(S\circ T = I\) is called the Inverse of \(T\) — Mizar says \(S\) is Reverse of \(T\). Missing from Mizar

The analogous definitions for matrices is found in (MATRIX_6:def 3) (MATRIX_6:def 2)

• Theorem 3.60. An invertible linear map has a unique inverse. Missing from Mizar
• Notation 3.61. We denote the inverse of \(T\) by \(T^{-1}\).
  • Mizar convention uses the notation T" for \(T^{-1}\)
• Theorem 3.63. A linear map is invertible if and only if it is injective and surjective.
  • FUNCT_2:25 proves this in general
• Theorem 3.65. Suppose \(V\) and \(W\) are finite-dimensional vector spaces and \(\dim(V)=\dim(W)\), and \(T\in\mathcal{L}(V,W)\). Then \(T\) is invertible iff \(T\) is injective iff \(T\) is surjective. Missing from Mizar
• Theorem 3.68. Suppose \(V\) and \(W\) are finite-dimensional vector spaces and \(\dim(V)=\dim(W)\), and \(S\in\mathcal{L}(V,W)\) and \(T\in\mathcal{L}(W,V)\). Then \(S\circ T=I\) if and only if \(T\circ S=I\). Missing from Mizar

• Definition 3.69.
  1. An Isomorphism is an invertible linear map.
  2. Two vector spaces are called Isomorphic if there is an isomorphism from one vector space to another.

• There doesn't seem to be are_isomorphic defined for vector spaces, so I'm marking this as Missing from Mizar
• Theorem 3.70. Two finite-dimensional vector spaces over \(\mathbb{F}\) are isomorphic if and only if they have the same dimension. Missing from Mizar
• Theorem 3.71. Suppose \(v_{1}\), …, \(v_{m}\) is a basis of \(V\) and \(w_{1}\), …, \(w_{n}\) is a basis of \(W\). Then \(\mathcal{M}\) is an isomorphism of \(\mathcal{L}(V,W)\) and \(\mathbb{F}^{m,n}\).
  • Missing from Mizar but I think MATRLIN and MATRLIN2 does a lot of the heavy lifting here.
• Theorem 3.72. Suppose \(V\) and \(W\) are finite-dimensional vector spaces. Then \(\mathcal{L}(V,W)\) is finite-dimensional and \(\dim\mathcal{L}(V,W)=(\dim V)(\dim W)\). Missing from Mizar

• Definition 3.73. Let \(v\in V\) and suppose \(b_{1}\), …, \(b_{n}\) be a basis for \(V\). Then we can form the Matrix associated to \(v\) relative to the basis by the n-by-1 matrix \(\mathcal{M}(v)=v_{1}b_{1}+\dots+v_{n}b_{n}\) where the scalars \(v_{1},\dots,v_{n}\in\mathbb{V}\) are the components of the n-vector.
  • This appears to be defined in MATRLIN:def 7 as v |-- b1 instead of \(\mathcal{M}(v)\).