Matrix.GeneralLinearGroup.IsEllipticdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
g is elliptic (from the name)
English
Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $R$. Then $g$ is elliptic, if the underlying value in the base of $g$ is elliptic.
Matrix.GeneralLinearGroup.IsHyperbolicdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
g is hyperbolic (from the name)
English
Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $R$. Then $g$ is hyperbolic, if the underlying value in the base of $g$ is hyperbolic.
Matrix.GeneralLinearGroup.IsParabolicdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
g is parabolic (from the name)
English
Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $R$. Then $g$ is parabolic, if the underlying value in the base of $g$ is parabolic.
Matrix.GeneralLinearGroup.fixpointPolynomialdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, function or constantWording
the fixpoint polynomial of g (from the name)
English
Let $g$ be a general linear group of $\mathrm{Fin}$ applied to $2$ and $R$. Then the fixpoint polynomial of $g$ is a polynomial of $R$ defined as the difference between the sum of the product of $\operatorname{C}$ applied to the underlying value in the base of $g$ and $\operatorname{X} ^ {2}$ and the product of $\operatorname{C}$ applied to the difference between the underlying value in the base of $g$ and the underlying value in the base of $g$ and $\operatorname{X}$ and $\operatorname{C}$ applied to the underlying value in the base of $g$.
Matrix.GeneralLinearGroup.upperRightHomdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, function or constantWording
the upper right homomorphism (from the name)
English
The upper right homomorphism is an additive characteristic of $R$ and the set of general linear groups of $\mathrm{Fin}$ applied to $2$ and $R$.
Matrix.IsEllipticdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
m is elliptic (from the name)
English
Let $m$ be a matrix of $\mathrm{Fin}$ applied to $2$ and $R$. Then $m$ is elliptic, if the discriminant of $m$ is less than $0$.
Matrix.IsHyperbolicdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
m is hyperbolic (from the name)
English
Let $m$ be a matrix of $\mathrm{Fin}$ applied to $2$ and $R$. Then $m$ is hyperbolic, if $0$ is less than the discriminant of $m$.
Matrix.IsParabolicdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, predicateWording
m is parabolic (from the name)
English
Let $m$ be a matrix of $\mathrm{Fin}$ applied to $2$ and $R$. Then $m$ is parabolic, if $m$ is not an element of the range of $\operatorname{coe}$ applied to the scalar of $\mathrm{Fin}$ applied to $2$ and the discriminant of $m$ is equal to $0$.
Matrix.parabolicEigenvaluedefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo, function or constantWording
the unique eigenvalue of m (from the docstring)
English
Let $m$ be a matrix of $\mathrm{Fin}$ applied to $2$ and $K$. Then the unique eigenvalue of $m$ is an element of $K$ defined as the quotient of the trace of $m$ and $2$.
Matrix.ProjGenLinGroupdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, typeWording
projection generator linear group of n and R (from the name)
English
Let $n$ and $R$ be sets. Then a projection generator linear group of $n$ and $R$ is an element of the function that maps $n$ and $R$ to the set of quotients of the set of general linear groups of $n$ and $R$ and the center of the set of general linear groups of $n$ and $R$.
Matrix.ProjGenLinGroup.liftdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantWording
the lift of f and hf (from the name)
English
Let $f$ be a monoid homomorphism of the set of general linear groups of $n$ and $R$ and $M$ such that the composition of $f$ and the scalar of $n$ is equal to $1$. Then the lift of $f$ and $\mathrm{hf}$ is a monoid homomorphism of the set of projection generator linear groups of $n$ and $R$ and $M$.
Matrix.ProjGenLinGroup.mapdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantWording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a monoid homomorphism of the set of projection generator linear groups of $n$ and $R$ and the set of projection generator linear groups of $n$ and $S$ defined as the map of the center of the set of general linear groups of $n$ and $S$ and the map of $f$.
Matrix.ProjGenLinGroup.mkdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantEnglish
$\operatorname{mk}$ is a monoid homomorphism of the set of general linear groups of $n$ and $R$ and the set of projection generator linear groups of $n$ and $R$ defined as $\operatorname{mk'}$ applied to the center of the set of general linear groups of $n$ and $R$.
Matrix.ProjGenLinGroup.signDetdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantWording
the sign determinant (from the name)
English
The sign determinant is a monoid homomorphism of the set of projection generator linear groups of $n$ and $R$ and the set of units of the set of sign types.
Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgCloseddefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantEnglish
$\operatorname{isoPSLOfAlgClosed}$ is a multiplicative equivalence of the set of projection generator linear groups of $n$ and $F$ and the set of projective special linear groups of $n$ and $F$.
Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedOfNonemptydefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantEnglish
$\operatorname{isoPSLOfAlgClosedOfNonempty}$ is a multiplicative equivalence of the set of projection generator linear groups of $n$ and $F$ and the set of projective special linear groups of $n$ and $F$.
Matrix.ProjectiveSpecialLinearGroup.toPGLdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantEnglish
$\operatorname{toPGL}$ is a monoid homomorphism of the set of projective special linear groups of $n$ and $R$ and the set of projection generator linear groups of $n$ and $R$.
Matrix.SpecialLinearGroup.toPGLdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective, function or constantEnglish
$\operatorname{toPGL}$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and the set of projection generator linear groups of $n$ and $R$ defined as the composition of $\operatorname{mk}$ and $\operatorname{toGL}$.
Matrix.hadamarddefMathlib.LinearAlgebra.Matrix.Hadamard, function or constantEnglish
Let $A$ and $B$ be matrixes of $n$ and $x$. Then there is a matrix of $n$ and $x$. Proof. Let $A$ be arbitrary. Let $B$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By A. By i1. By j1. By B. By times. By Matrix__of__app.
Matrix.IsHadamardstructureMathlib.LinearAlgebra.Matrix.HadamardMatrix, predicateEnglish
Let $A$ be a matrix of $n$ and $R$. Then we can say that $\operatorname{IsHadamard}$ holds for $A$.
Matrix.IsHermitiandefMathlib.LinearAlgebra.Matrix.Hermitian, predicateWording
A is hermitian (from the name)
English
Let $A$ be a matrix of $n$ and $x$. Then $A$ is hermitian, if the conjugate transpose of $A$ is equal to $A$.
Matrix.IsUpperHessenbergdefMathlib.LinearAlgebra.Matrix.Hessenberg.Defs, predicateEnglish
Let $M$ be a matrix of $m$ and $R$. Then $\operatorname{IsUpperHessenberg}$ holds for $M$, if for all elements $i$ and $j$ of $m$, if the successor of $j$ is less than $i$, then $\EqtMACRoH {M (i , j)}{0}$.
Matrix.Hessenberg.SimilaritystructureMathlib.LinearAlgebra.Matrix.Hessenberg.Similarity, typeWording
similarity of A (from the name)
English
Let $A$ be a matrix of $m$ and $R$. Then the similarities of $A$ are a basic type.
Matrix.Hessenberg.Similarity.HdefMathlib.LinearAlgebra.Matrix.Hessenberg.Similarity, function or constantEnglish
Let $\mathrm{self}$ be a similarity of $A$. Then there is a matrix of $m$ and $R$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By Matrix__Hessenberg__Similarity__proj2.
Matrix.Hessenberg.Similarity.LdefMathlib.LinearAlgebra.Matrix.Hessenberg.Similarity, function or constantEnglish
Let $\mathrm{self}$ be a similarity of $A$. Then there is a matrix of $m$ and $R$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By Matrix__Hessenberg__Similarity__proj0.
Matrix.Hessenberg.Similarity.σdefMathlib.LinearAlgebra.Matrix.Hessenberg.Similarity, function or constantEnglish
Let $\mathrm{self}$ be a similarity of $A$. Then $\mathrm{Matrix\_\_Hessenberg\_\_Similarity\_\_\_u3c3\_}$ applied to $\mathrm{self}$ is a permutation of $m$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Ideal.matrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the matrix of n and I (from the name)
English
Let $n$ be a set. Let $I$ be an ideal of $R$. Then the matrix of $n$ and $I$ is an ideal of the set of matrixes of $n$ and $R$.
RingCon.matrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the matrix of n and c (from the name)
English
Let $n$ be a set. Let $c$ be a ring congruence relation of $R$. Then the matrix of $n$ and $c$ is a ring congruence relation of the set of matrixes of $n$ and $R$.
RingCon.ofMatrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the ring congruence relation of c (from the name)
English
Let $c$ be a ring congruence relation of the set of matrixes of $n$ and $R$. Then the ring congruence relation of $c$ is a ring congruence relation of $R$.
TwoSidedIdeal.equivMatrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the equivalence matrix (from the name)
English
The equivalence matrix is an equivalence from $\mathrm{TwoSidedIdeal}$ applied to $R$ to $\mathrm{TwoSidedIdeal}$ applied to the set of matrixes of $n$ and $R$.
TwoSidedIdeal.matrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the matrix of n and I (from the name)
English
Let $n$ be a set. Let $I$ be an element of $\mathrm{TwoSidedIdeal}$ applied to $R$. Then the matrix of $n$ and $I$ is an element of $\mathrm{TwoSidedIdeal}$ applied to the set of matrixes of $n$ and $R$ defined as $\operatorname{ofRingCon}$ applied to the matrix of $n$ and the ring congruence relation of $I$.
TwoSidedIdeal.orderIsoMatrixdefMathlib.LinearAlgebra.Matrix.Ideal, function or constantWording
the order isomorphism matrix (from the name)
English
The order isomorphism matrix is an order isomorphism of $\mathrm{TwoSidedIdeal}$ applied to $R$ and $\mathrm{TwoSidedIdeal}$ applied to the set of matrixes of $n$ and $R$.
Matrix.dendefMathlib.LinearAlgebra.Matrix.Integer, function or constantWording
the denominator of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $\Rational$. Then the denominator of $A$ is a natural number defined as the least common multiple of the universal set and the function that maps $P$ to $\operatorname{den}$ applied to $A$ applied to $\ProdfstMACRoZ {P}$ and $\ProdsndMACRoAA {P}$.
Matrix.numdefMathlib.LinearAlgebra.Matrix.Integer, function or constantWording
the numerator of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $\Rational$. Then the numerator of $A$ is a matrix of $n$ and $\Integer$ defined as the map of $\HSMulhSMulMACRoAL {\operatorname{den} (A)}{A}$ and $\operatorname{num}$.
Matrix.transposeInvertibleEquivInvertibledefMathlib.LinearAlgebra.Matrix.Invertible, function or constantEnglish
Let $A$ be a matrix of $n$ and $x$. Then $\operatorname{transposeInvertibleEquivInvertible}$ applied to $A$ is an equivalence from the proposition that the transpose of $A$ is invertible to the proposition that $A$ is invertible.
Matrix.IsIrreduciblestructureMathlib.LinearAlgebra.Matrix.Irreducible.Defs, predicateWording
A is irreducible (from the name)
English
Let $A$ be a matrix of $n$ and $R$. Then we can say that $A$ is irreducible.
Matrix.IsPrimitivestructureMathlib.LinearAlgebra.Matrix.Irreducible.Defs, predicateWording
A is primitive (from the name)
English
Let $A$ be a matrix of $n$ and $R$. Then we can say that $A$ is primitive.
Matrix.transposePathdefMathlib.LinearAlgebra.Matrix.Irreducible.Defs, function or constantWording
the transpose path of p (from the name)
English
Let $p$ be a path of $i$ and $j$. Then the transpose path of $p$ is a path of $j$ and $i$.
Matrix.IsDiagdefMathlib.LinearAlgebra.Matrix.IsDiag, predicateWording
A is a diagonal (from the name)
English
Let $A$ be a matrix of $n$ and $x$. Then $A$ is a diagonal, if the function that maps $i$ and $j$ to $\EqtMACRoH {A (i , j)}{0}$ is pairwise.
Matrix.kroneckerdefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantWording
the Kronecker product of x2 and x3 (from the docstring)
English
Let $x_{2}$ be a matrix of $m$ and $x$. Let $x_{3}$ be a matrix of $p$ and $x$. Then the Kronecker product of $x_{2}$ and $x_{3}$ is a matrix of $\mathrm{Prod}$ applied to $m$ and $p$ and $x$ defined as $\operatorname{kroneckerMap}$ applied to the function that maps $x_{2}$ and $x_{3}$ to $x_{2} \times x_{3}$, $x_{2}$ and $x_{3}$.
Matrix.kroneckerBilineardefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantEnglish
$\operatorname{kroneckerBilinear}$ is a linear map of the set of matrixes of $m$ and $x$ and the set of linear maps of the set of matrixes of $p$ and $x$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $p$ and $x$ defined as $\operatorname{kroneckerMapBilinear}$ applied to the linear map of $\operatorname{lmul}$ applied to $R$ and $x$.
Matrix.kroneckerMapdefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantEnglish
Let $f$ be a function from elements of $x$ and elements of $x_{1}$ to elements of $x_{2}$. Let $A$ be a matrix of $m$ and $x$. Let $B$ be a matrix of $p$ and $x_{1}$. Then there is a matrix of $\mathrm{Prod}$ applied to $m$ and $p$ and $x_{2}$. Proof. Let $f$ be arbitrary. Let $A$ be arbitrary. Let $B$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By Prod__fst. By j1. By Prod__fst. By A. By i1. By Prod__snd. By j1. By Prod__snd. By B. By f. By Matrix__of__app.
Matrix.kroneckerMapBilineardefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantEnglish
Let $f$ be a linear map of $x$ and the set of linear maps of $x_{1}$ and $x_{2}$. Then $\operatorname{kroneckerMapBilinear}$ applied to $f$ is a linear map of the set of matrixes of $m$ and $x$ and the set of linear maps of the set of matrixes of $p$ and $x_{1}$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $p$ and $x_{2}$.
Matrix.kroneckerTMuldefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantEnglish
Let $R$ be a set. Let $x_{7}$ be a matrix of $m$ and $x$. Let $x_{8}$ be a matrix of $p$ and $x_{1}$. Then there is a matrix of $\mathrm{Prod}$ applied to $m$ and $p$ and the set of tensor products of $x$ and $x_{1}$. Proof. Let $R$ be arbitrary. Let $x_{7}$ be arbitrary. Let $x_{8}$ be arbitrary. Let $x_{7}$ be arbitrary. Let $x_{8}$ be arbitrary. By R. By x7. By x8. By TensorProduct__tmul. By x7. By x8. By Matrix__kroneckerMap.
Matrix.kroneckerTMulBilineardefMathlib.LinearAlgebra.Matrix.Kronecker, function or constantEnglish
Let $R$ and $S$ be sets. Then $\operatorname{kroneckerTMulBilinear}$ applied to $R$ and $S$ is a linear map of the set of matrixes of $m$ and $x$ and the set of linear maps of the set of matrixes of $p$ and $x_{1}$ and the set of matrixes of $\mathrm{Prod}$ applied to $m$ and $p$ and the set of tensor products of $x$ and $x_{1}$ defined as $\operatorname{kroneckerMapBilinear}$ applied to $\operatorname{mk}$ applied to $R$, $S$, $x$ and $x_{1}$.
LinearMap.mapMatrixModuledefMathlib.LinearAlgebra.Matrix.Module, function or constantWording
the map matrix module of x and f (from the name)
English
Let $x$ be a set. Let $f$ be a linear map of $M$ and $N$. Then the map matrix module of $x$ and $f$ is a linear map of the set of functions from elements of $x$ to elements of $M$ and the set of functions from elements of $x$ to elements of $N$.
Matrix.mvPolynomialXdefMathlib.LinearAlgebra.Matrix.MvPolynomial, function or constantWording
the multivariate polynomial of n and R (from the name)
English
Let $m$, $n$ and $R$ be sets. Then the multivariate polynomial of $n$ and $R$ is a matrix of $n$ and the set of multivariate polynomials of $\mathrm{Prod}$ applied to $m$ and $n$ and $R$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\operatorname{X}$ applied to $\ProdmkMACRoU {i_{1}}{j_{1}}$.
Matrix.NondegeneratestructureMathlib.LinearAlgebra.Matrix.Nondegenerate, predicateWording
M is a nondegenerate (from the name)
English
Let $M$ be a matrix of $n$ and $R$. Then we can say that $M$ is a nondegenerate.
Matrix.SeparatingLeftdefMathlib.LinearAlgebra.Matrix.Nondegenerate, predicateWording
M is a left separating (from the name)
English
Let $M$ be a matrix of $n$ and $R$. Then $M$ is a left separating, if for all functions $v$ from elements of $m$ to elements of $R$, if for all functions $w$ from elements of $n$ to elements of $R$, the sum of the entrywise products of $v$ and $\operatorname{mulVec}$ applied to $w$ is equal to $0$, then $\EqtMACRoH {v}{0}$.
Matrix.SeparatingRightdefMathlib.LinearAlgebra.Matrix.Nondegenerate, predicateWording
M is a right separating (from the name)
English
Let $M$ be a matrix of $n$ and $R$. Then $M$ is a right separating, if for all functions $w$ from elements of $n$ to elements of $R$, if for all functions $v$ from elements of $m$ to elements of $R$, the sum of the entrywise products of $v$ and $\operatorname{mulVec}$ applied to $w$ is equal to $0$, then $\EqtMACRoH {w}{0}$.
Matrix.diagonalInvertibleEquivInvertibledefMathlib.LinearAlgebra.Matrix.NonsingularInverse, function or constantEnglish
Let $v$ be a function from elements of $n$ to elements of $x$. Then $\operatorname{diagonalInvertibleEquivInvertible}$ applied to $v$ is an equivalence from the proposition that the diagonal of $v$ is invertible to the proposition that $v$ is invertible.
Matrix.invertibleEquivDetInvertibledefMathlib.LinearAlgebra.Matrix.NonsingularInverse, function or constantEnglish
Let $A$ be a matrix of $n$ and $x$. Then $\operatorname{invertibleEquivDetInvertible}$ applied to $A$ is an equivalence from the proposition that $A$ is invertible to the proposition that the determinant of $A$ is invertible.
Matrix.nonsingInvUnitdefMathlib.LinearAlgebra.Matrix.NonsingularInverse, function or constantEnglish
Let $A$ be a matrix of $n$ and $x$ such that the determinant of $A$ is a unit. Then $\operatorname{nonsingInvUnit}$ applied to $A$ and $h$ is a unit of the set of matrixes of $n$ and $x$ defined as the unit of $A$.
Matrix.submatrixEquivInvertibleEquivInvertibledefMathlib.LinearAlgebra.Matrix.NonsingularInverse, function or constantEnglish
Let $A$ be a matrix of $m$ and $x$. Let $x_{6}$ and $x_{7}$ be equivalences from $n$ to $m$. Then $\operatorname{submatrixEquivInvertibleEquivInvertible}$ applied to $A$, $x_{6}$ and $x_{7}$ is an equivalence from the proposition that the submatrix of $\operatorname{coe}$ applied to $x_{6}$ and $\operatorname{coe}$ applied to $x_{7}$ is invertible to the proposition that $A$ is invertible.
Matrix.unitOfDetInvertibledefMathlib.LinearAlgebra.Matrix.NonsingularInverse, function or constantWording
the unit of A (from the name)
English
Let $A$ be a matrix of $n$ and $x$. Then the unit of $A$ is a unit of the set of matrixes of $n$ and $x$ defined as the unit of $A$.
Matrix.matrixNotationdefMathlib.LinearAlgebra.Matrix.Notation, function or constantWording
the matrix notation (from the name)
English
generation took over the time limit
Matrix.matrixNotation0xCdefMathlib.LinearAlgebra.Matrix.Notation, function or constantWording
the matrix notation (from the name)
English
generation took over the time limit
Matrix.matrixNotationRx0defMathlib.LinearAlgebra.Matrix.Notation, function or constantEnglish
generation took over the time limit
Matrix.mkLiteralQdefMathlib.LinearAlgebra.Matrix.Notation, function or constantEnglish
generation took over the time limit
Matrix.HasOrthogonalColsdefMathlib.LinearAlgebra.Matrix.Orthogonal, predicateEnglish
Let $A$ be a matrix of $n$ and $x$. Then $\operatorname{HasOrthogonalCols}$ holds for $A$, if the transpose of $A$ has orthogonal rows.
Matrix.HasOrthogonalRowsdefMathlib.LinearAlgebra.Matrix.Orthogonal, predicateWording
A has orthogonal rows (from the name)
English
Let $A$ be a matrix of $n$ and $x$. Then $A$ has orthogonal rows, if for all elements $x_{4}$ and $x_{5}$ of $m$, if $x_{4} \neq x_{5}$, then the sum of the entrywise products of $A$ applied to $x_{4}$ and $A$ applied to $x_{5}$ is equal to $0$.
Matrix.permanentdefMathlib.LinearAlgebra.Matrix.Permanent, function or constantEnglish
Let $M$ be a matrix of $n$ and $R$. Then $\operatorname{permanent}$ applied to $M$ is an element of $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{x_{3}}{(\FinsetProd {\FinsetunivMACRoAC}{i}{M (x_{3} (i), i)})}$.
Equiv.Perm.permMatrixdefMathlib.LinearAlgebra.Matrix.Permutation, function or constantWording
the permutation matrix of R and x1 (from the name)
English
Let $R$ be a set. Let $x_{1}$ be a permutation of $n$. Then the permutation matrix of $R$ and $x_{1}$ is a matrix of $n$ and $R$ defined as the matrix of the equivalence of $x_{1}$.
Matrix.permMatrixHomdefMathlib.LinearAlgebra.Matrix.Permutation, function or constantWording
the permutation matrix homomorphism (from the name)
English
The permutation matrix homomorphism is a monoid homomorphism of the set of permutations of $n$ and the set of matrixes of $n$ and $R$.
Matrix.PosDefdefMathlib.LinearAlgebra.Matrix.PosDef, predicateWording
M is a positive part (from the name)
English
Let $M$ be a matrix of $n$ and $R$. Then $M$ is a positive part, if $M$ is hermitian and for all elements $x_{3}$ of $\FinsuppMACRoQ {n}{R}$, if $x_{3} \neq 0$, then $0$ is less than the sum of $x_{3}$ and the function that maps $i$ and $\xi$ to the sum of $x_{3}$ and the function that maps $j$ and $\mathrm{xj}$ to the product of the product of the star of $\xi$ and $M$ applied to $i$ and $j$ and $\mathrm{xj}$.
Matrix.PosSemidefdefMathlib.LinearAlgebra.Matrix.PosDef, predicateEnglish
Let $M$ be a matrix of $n$ and $R$. Then $\operatorname{PosSemidef}$ holds for $M$, if $M$ is hermitian and for all elements $x_{3}$ of $\FinsuppMACRoQ {n}{R}$, $0$ is less than or equal to the sum of $x_{3}$ and the function that maps $i$ and $\xi$ to the sum of $x_{3}$ and the function that maps $j$ and $\mathrm{xj}$ to the product of the product of the star of $\xi$ and $M$ applied to $i$ and $j$ and $\mathrm{xj}$.
Matrix.ProjectiveSpecialLinearGroupdefMathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup, typeWording
projective special linear group of n and R (from the name)
English
Let $n$ and $R$ be sets. Then a projective special linear group of $n$ and $R$ is an element of the function that maps $n$ and $R$ to the set of quotients of the set of special linear groups of $n$ and $R$ and the center of the set of special linear groups of $n$ and $R$.
Matrix.cRankdefMathlib.LinearAlgebra.Matrix.Rank, function or constantWording
the rank of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $R$. Then the rank of $A$ is a cardinal defined as the rank of $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{range} (\operatorname{col} (A)))}{x_{1}})}$.
Matrix.eRankdefMathlib.LinearAlgebra.Matrix.Rank, function or constantWording
the rank of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $R$. Then the rank of $A$ is a natural number defined as $\operatorname{toENat}$ applied to the rank of $A$.
Matrix.rankdefMathlib.LinearAlgebra.Matrix.Rank, function or constantWording
the rank of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $R$. Then the rank of $A$ is an element of $\Natural$ defined as the rank of $R$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{mulVecLin} (A))}{x_{2}})}$.
Matrix.reindexAddEquivdefMathlib.LinearAlgebra.Matrix.Reindex, function or constantWording
the reindexing additive equivalence of x1 and x2 (from the name)
English
Let $R$ be a set. Let $x_{1}$ be an equivalence from $m$ to $\mathrm{m'}$. Let $x_{2}$ be an equivalence from $n$ to $\mathrm{n'}$. Then the reindexing additive equivalence of $x_{1}$ and $x_{2}$ is an additive equivalence of the set of matrixes of $n$ and $R$ and the set of matrixes of $\mathrm{n'}$ and $R$.
Matrix.reindexAlgEquivdefMathlib.LinearAlgebra.Matrix.Reindex, function or constantWording
the reindexing algebra isomorphism of e (from the name)
English
Let $R$ and $A$ be sets. Let $e$ be an equivalence from $m$ to $n$. Then the reindexing algebra isomorphism of $e$ is an algebra isomorphism of the set of matrixes of $m$ and $A$ and the set of matrixes of $n$ and $A$.
Matrix.reindexLinearEquivdefMathlib.LinearAlgebra.Matrix.Reindex, function or constantWording
the reindexing linear equivalence of x3 and x4 (from the name)
English
Let $R$ and $A$ be sets. Let $x_{3}$ be an equivalence from $m$ to $\mathrm{m'}$. Let $x_{4}$ be an equivalence from $n$ to $\mathrm{n'}$. Then the reindexing linear equivalence of $x_{3}$ and $x_{4}$ is a linear equivalence of the set of matrixes of $n$ and $A$ and the set of matrixes of $\mathrm{n'}$ and $A$.
Matrix.reindexRingEquivdefMathlib.LinearAlgebra.Matrix.Reindex, function or constantWording
the reindexing ring isomorphism of R and e (from the name)
English
Let $R$ be a set. Let $e$ be an equivalence from $m$ to $n$. Then the reindexing ring isomorphism of $R$ and $e$ is a ring isomorphism of the set of matrixes of $m$ and $R$ and the set of matrixes of $n$ and $R$.
Matrix.replicateColdefMathlib.LinearAlgebra.Matrix.RowCol, function or constantEnglish
Let $x_{1}$ be a set. Let $w$ be a function from elements of $m$ to elements of $x$. Then there is a matrix of $x_{1}$ and $x$. Proof. Let $x_{1}$ be arbitrary. Let $w$ be arbitrary. Let $x_{4}$ be arbitrary. Let $x_{5}$ be arbitrary. By x4. By w. By Matrix__of__app.
Matrix.replicateRowdefMathlib.LinearAlgebra.Matrix.RowCol, function or constantEnglish
Let $x_{1}$ be a set. Let $v$ be a function from elements of $n$ to elements of $x$. Then there is a matrix of $n$ and $x$. Proof. Let $x_{1}$ be arbitrary. Let $v$ be arbitrary. Let $x_{3}$ be arbitrary. Let $y_{1}$ be arbitrary. By y1. By v. By Matrix__of__app.
Matrix.updateColdefMathlib.LinearAlgebra.Matrix.RowCol, function or constantEnglish
Let $M$ be a matrix of $n$ and $x$. Let $j$ be an element of $n$. Let $b$ be a function from elements of $m$ to elements of $x$. Then there is a matrix of $n$ and $x$. Proof. Let $M$ be arbitrary. Let $j$ be arbitrary. Let $b$ be arbitrary. Let $i_{1}$ be arbitrary. By i1. By M. By j. By i1. By b. By Function__update. By Matrix__of__app.
Matrix.updateRowdefMathlib.LinearAlgebra.Matrix.RowCol, function or constantEnglish
Let $M$ be a matrix of $n$ and $x$. Let $i$ be an element of $m$. Let $b$ be a function from elements of $n$ to elements of $x$. Then there is a matrix of $n$ and $x$. Proof. Let $M$ be arbitrary. Let $i$ be arbitrary. Let $b$ be arbitrary. By M. By i. By b. By Function__update. By Matrix__of__app.
Matrix.fromBlocksZero₁₂InvertibleEquivdefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ and $C$ be matrixes of $m$ and $x$. Let $D$ be a matrix of $n$ and $x$. Then $\mathrm{Matrix\_\_fromBlocksZero\_u2081\_\_u2082\_InvertibleEquiv}$ applied to $A$, $C$ and $D$ is an equivalence from the proposition that $\operatorname{fromBlocks}$ applied to $A$, $0$, $C$ and $D$ is invertible to $\mathrm{Prod}$ applied to the proposition that $A$ is invertible and the proposition that $D$ is invertible.
Matrix.fromBlocksZero₂₁InvertibleEquivdefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ be a matrix of $m$ and $x$. Let $B$ and $D$ be matrixes of $n$ and $x$. Then $\mathrm{Matrix\_\_fromBlocksZero\_u2082\_\_u2081\_InvertibleEquiv}$ applied to $A$, $B$ and $D$ is an equivalence from the proposition that $\operatorname{fromBlocks}$ applied to $A$, $B$, $0$ and $D$ is invertible to $\mathrm{Prod}$ applied to the proposition that $A$ is invertible and the proposition that $D$ is invertible.
Matrix.invertibleEquivFromBlocks₁₁InvertibledefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ and $C$ be matrixes of $m$ and $x$. Let $B$ and $D$ be matrixes of $n$ and $x$. Then $\mathrm{Matrix\_\_invertibleEquivFromBlocks\_u2081\_\_u2081\_Invertible}$ applied to $A$, $B$, $C$ and $D$ is an equivalence from the proposition that $\operatorname{fromBlocks}$ applied to $A$, $B$, $C$ and $D$ is invertible to the proposition that the difference between $D$ and the product of $C$, the inverse of $A$ and $B$ is invertible.
Matrix.invertibleEquivFromBlocks₂₂InvertibledefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ and $C$ be matrixes of $m$ and $x$. Let $B$ and $D$ be matrixes of $n$ and $x$. Then $\mathrm{Matrix\_\_invertibleEquivFromBlocks\_u2082\_\_u2082\_Invertible}$ applied to $A$, $B$, $C$ and $D$ is an equivalence from the proposition that $\operatorname{fromBlocks}$ applied to $A$, $B$, $C$ and $D$ is invertible to the proposition that the difference between $A$ and the product of $B$, the inverse of $D$ and $C$ is invertible.
Matrix.invertibleOfFromBlocksZero₁₂InvertibledefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ and $C$ be matrixes of $m$ and $x$. Let $D$ be a matrix of $n$ and $x$. Then $\mathrm{Matrix\_\_invertibleOfFromBlocksZero\_u2081\_\_u2082\_Invertible}$ applied to $A$, $C$ and $D$ is an element of $\mathrm{Prod}$ applied to the proposition that $A$ is invertible and the proposition that $D$ is invertible.
Matrix.invertibleOfFromBlocksZero₂₁InvertibledefMathlib.LinearAlgebra.Matrix.SchurComplement, function or constantEnglish
Let $A$ be a matrix of $m$ and $x$. Let $B$ and $D$ be matrixes of $n$ and $x$. Then $\mathrm{Matrix\_\_invertibleOfFromBlocksZero\_u2082\_\_u2081\_Invertible}$ applied to $A$, $B$ and $D$ is an element of $\mathrm{Prod}$ applied to the proposition that $A$ is invertible and the proposition that $D$ is invertible.
Matrix.IsDetpBalanceddefMathlib.LinearAlgebra.Matrix.SemiringInverse, predicateEnglish
Let $A$ be a matrix of $n$ and $R$. Let $a$ and $b$ be elements of $R$. Then $\operatorname{IsDetpBalanced}$ holds for $A$, $a$ and $b$, if $\EqtMACRoH {a \times \operatorname{detp} (1 , A)+ b \times \operatorname{detp} (\operatorname{neg} (1), A)}{b \times \operatorname{detp} (1 , A)+ a \times \operatorname{detp} (\operatorname{neg} (1), A)}$.
Matrix.NonsingulardefMathlib.LinearAlgebra.Matrix.SemiringInverse, predicateWording
A is nonsingular (from the name)
English
Let $A$ be a matrix of $n$ and $R$. Then $A$ is nonsingular, if for all elements $a$ and $b$ of $R$, if $\operatorname{IsDetpBalanced}$ holds for $A$, $a$ and $b$, then $\EqtMACRoH {a}{b}$.
Matrix.adjpdefMathlib.LinearAlgebra.Matrix.SemiringInverse, function or constantEnglish
Let $s$ be an element of $\UnitsMACRoAO {\Integer}$. Let $A$ be a matrix of $n$ and $R$. Then there is a matrix of $n$ and $R$. Proof. Let $s$ be arbitrary. Let $A$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. Let $x_{3}$ be arbitrary. By j1. By x3. By i1. By Eqt. By s. By Equiv__Perm__ofSign. By Finset__filter. Let $x_{4}$ be arbitrary. By j1. By Singleton__singleton. By Compl__compl. Let $k$ be arbitrary. By k. By k. By x4. By A. By Finset__prod. By Finset__sum. By Matrix__of__app.
Matrix.detpdefMathlib.LinearAlgebra.Matrix.SemiringInverse, function or constantEnglish
Let $s$ be an element of $\UnitsMACRoAO {\Integer}$. Let $A$ be a matrix of $n$ and $R$. Then $\operatorname{detp}$ applied to $s$ and $A$ is an element of $R$ defined as $\FinsetSum {\operatorname{ofSign} (s)}{x_{3}}{(\FinsetProd {\FinsetunivMACRoAC}{k}{A (k , x_{3} (k))})}$.
LinearMap.toMatrix₂defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the matrix of x16 and x17 (from the name)
English
Let $x_{16}$ be a basis of $R$ and $x$. Let $x_{17}$ be a basis of $R$ and $x_{1}$. Then the matrix of $x_{16}$ and $x_{17}$ is a linear equivalence of the set of linear maps of $x$ and the set of linear maps of $x_{1}$ and $x_{2}$ and the set of matrixes of $m$ and $x_{2}$ defined as the composition of the arrow congruence of the equivalence function of $x_{16}$ and the arrow congruence of the equivalence function of $x_{17}$ and the identity map of $R$ and $x_{2}$ and the matrix of $R$.
LinearMap.toMatrix₂'defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the matrix of R (from the name)
English
Let $R$ be a set. Then the matrix of $R$ is a linear equivalence of the set of linear maps of the set of functions from elements of $n$ to elements of $x$ and the set of linear maps of the set of functions from elements of $m$ to elements of $x_{1}$ and $x_{2}$ and the set of matrixes of $m$ and $x_{2}$ defined as the matrix of $R$.
LinearMap.toMatrixₛₗ₂'defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the matrix of R (from the name)
English
Let $R$ be a set. Then the matrix of $R$ is a linear equivalence of the set of linear maps of the set of functions from elements of $n$ to elements of $x$ and the set of linear maps of the set of functions from elements of $m$ to elements of $x_{2}$ and $x_{4}$ and the set of matrixes of $m$ and $x_{4}$.
Matrix.IsAdjointPairdefMathlib.LinearAlgebra.Matrix.SesquilinearForm, predicateEnglish
Let $J$ and $A$ be matrixes of $n$ and $R$. Let $\mathrm{J'}$ and $\mathrm{A'}$ be matrixes of $\mathrm{n'}$ and $R$. Then $\operatorname{IsAdjointPair}$ holds for $J$, $\mathrm{J'}$, $A$ and $\mathrm{A'}$, if the product of the transpose of $A$ and $\mathrm{J'}$ is equal to $J \times \mathrm{A'}$.
Matrix.IsSelfAdjointdefMathlib.LinearAlgebra.Matrix.SesquilinearForm, predicateEnglish
Let $J$ and $x_{2}$ be matrixes of $n$ and $R$. Then $\operatorname{IsSelfAdjoint}$ holds for $J$ and $x_{2}$, if $\operatorname{IsAdjointPair}$ holds for $J$, $J$, $x_{2}$ and $x_{2}$.
Matrix.IsSkewAdjointdefMathlib.LinearAlgebra.Matrix.SesquilinearForm, predicateEnglish
Let $J$ and $x_{2}$ be matrixes of $n$ and $R$. Then $\operatorname{IsSkewAdjoint}$ holds for $J$ and $x_{2}$, if $\operatorname{IsAdjointPair}$ holds for $J$, $J$, $x_{2}$ and $\operatorname{neg}$ applied to $x_{2}$.
Matrix.toLinearMap₂defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the linear map of x14 and x15 (from the name)
English
Let $x_{14}$ be a basis of $R$ and $x$. Let $x_{15}$ be a basis of $R$ and $x_{1}$. Then the linear map of $x_{14}$ and $x_{15}$ is a linear equivalence of the set of matrixes of $m$ and $x_{2}$ and the set of linear maps of $x$ and the set of linear maps of $x_{1}$ and $x_{2}$ defined as the linear map of $x_{14}$ and $x_{15}$.
Matrix.toLinearMap₂'defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the linear map of R (from the name)
English
Let $R$ be a set. Then the linear map of $R$ is a linear equivalence of the set of matrixes of $m$ and $x_{2}$ and the set of linear maps of the set of functions from elements of $n$ to elements of $x$ and the set of linear maps of the set of functions from elements of $m$ to elements of $x_{1}$ and $x_{2}$ defined as the inverse of the matrix of $R$.
Matrix.toLinearMapₛₗ₂defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the linear map of x15 and x16 (from the name)
English
Let $x_{10}$ be a ring homomorphism of $R$ and $R$. Let $x_{15}$ be a basis of $R$ and $x$. Let $x_{16}$ be a basis of $R$ and $x_{1}$. Then the linear map of $x_{15}$ and $x_{16}$ is a linear equivalence of the set of matrixes of $m$ and $x_{2}$ and the set of linear maps of $x$ and the set of linear maps of $x_{1}$ and $x_{2}$ defined as the inverse of the matrix of $x_{15}$ and $x_{16}$.
Matrix.toLinearMapₛₗ₂'defMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the linear map of x14 and x15 (from the name)
English
Let $R$ be a set. Let $x_{14}$ be a ring homomorphism of $x$ and $x_{1}$. Let $x_{15}$ be a ring homomorphism of $x_{2}$ and $x_{3}$. Then the linear map of $x_{14}$ and $x_{15}$ is a linear equivalence of the set of matrixes of $m$ and $x_{4}$ and the set of linear maps of the set of functions from elements of $n$ to elements of $x$ and the set of linear maps of the set of functions from elements of $m$ to elements of $x_{2}$ and $x_{4}$ defined as the inverse of the matrix of $R$.
pairSelfAdjointMatricesSubmoduledefMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the pair self adjoint matrice submodule of J and x2 (from the name)
English
Let $J$ and $x_{2}$ be matrixes of $n$ and $R$. Then the pair self adjoint matrice submodule of $J$ and $x_{2}$ is a submodule of $R$ and the set of matrixes of $n$ and $R$ defined as the map of $\operatorname{toLinearMap}$ applied to the matrix and $\operatorname{isPairSelfAdjointSubmodule}$ applied to $\mathrm{Matrix\_\_toLinearMap\_u2082\_'\_\_app}$ applied to $R$ and $J$ and $\mathrm{Matrix\_\_toLinearMap\_u2082\_'\_\_app}$ applied to $R$ and $x_{2}$.
selfAdjointMatricesSubmoduledefMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the self adjoint matrice submodule of J (from the name)
English
Let $J$ be a matrix of $n$ and $R$. Then the self adjoint matrice submodule of $J$ is a submodule of $R$ and the set of matrixes of $n$ and $R$ defined as the pair self adjoint matrice submodule of $J$ and $J$.
skewAdjointMatricesSubmoduledefMathlib.LinearAlgebra.Matrix.SesquilinearForm, function or constantWording
the skew adjoint matrice submodule of J (from the name)
English
Let $J$ be a matrix of $n$ and $R$. Then the skew adjoint matrice submodule of $J$ is a submodule of $R$ and the set of matrixes of $n$ and $R$ defined as the pair self adjoint matrice submodule of $\operatorname{neg}$ applied to $J$ and $J$.
Matrix.SpecialLinearGroupdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, typeWording
special linear group of n and R (from the name)
English
Let $n$ and $R$ be sets. Then a special linear group of $n$ and $R$ is an element of the function that maps $n$ and $R$ to $\SubtypeSet {A}{(\EqtMACRoH {\operatorname{det} (A)}{1})}$.
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnitydefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the center equivalence root (from the name)
English
The center equivalence root is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (\operatorname{SpecialLinearGroup} (n , R))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\MaxmaxMACRoAF {\operatorname{card} (n)}{1}, R)}{x_{4}})}$.
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'defMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the center equivalence root of i (from the name)
English
Let $i$ be an element of $n$. Then the center equivalence root of $i$ is a multiplicative equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (\operatorname{SpecialLinearGroup} (n , R))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\operatorname{card} (n), R)}{x_{4}})}$.
Matrix.SpecialLinearGroup.coeMonoidHomdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the coercion monoid homomorphism (from the name)
English
The coercion monoid homomorphism is a monoid homomorphism of the set of special linear groups of $x$ and $R$ and the set of matrixes of $x$ and $R$.
Matrix.SpecialLinearGroup.diag2defMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the diagonal of a and ha (from the name)
English
Let $a$ be an element of $F$ such that $a \neq 0$. Then the diagonal of $a$ and $\mathrm{ha}$ is a special linear group of $\mathrm{Fin}$ applied to $2$ and $F$.
Matrix.SpecialLinearGroup.diag2ndefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the diagonal of a (from the name)
English
Assume that $i \neq j$. Let $a$ be an element of $F$ such that $a \neq 0$. Then the diagonal of $a$ is a special linear group of $x_{1}$ and $F$ defined as the diagonal of the function that maps $k$ to $\iteMACRoG {(\EqtMACRoH {k}{i})}{a}{(\iteMACRoG {(\EqtMACRoH {k}{j})}{\operatorname{inv} (a)}{1})}$.
Matrix.SpecialLinearGroup.mapdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the map of f (from the name)
English
Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and the set of special linear groups of $n$ and $S$.
Matrix.SpecialLinearGroup.toLin'defMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantEnglish
$\operatorname{toLin'}$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and the set of linear equivalences of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$.
Matrix.SpecialLinearGroup.transposedefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the transpose in A (from the docstring)
English
Let $A$ be a special linear group of $n$ and $R$. Then the transpose in $A$ is a special linear group of $n$ and $R$ defined as the transpose of $A$.
Matrix.SpecialLinearGroup.transvectiondefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the transvection of hij and b (from the docstring)
English
Assume that $i \neq j$. Let $b$ be an element of $F$. Then the transvection of $\mathrm{hij}$ and $b$ is a special linear group of $x$ and $F$ defined as the transvection of $j$ and $b$.
Matrix.TransvectionStruct.toSpecialLinearGroupdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantWording
the special linear group of t (from the name)
English
Let $t$ be an element of $\operatorname{TransvectionStruct}$ applied to $x$ and $F$. Then the special linear group of $t$ is a special linear group of $x$ and $F$ defined as the transvection of $\operatorname{hij}$ applied to $t$ and $\operatorname{c}$ applied to $t$.
ModularGroup.SdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantEnglish
$\operatorname{S}$ is a special linear group of $\mathrm{Fin}$ applied to $2$ and $\Integer$ defined as $\operatorname{of}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecEmpty}$ and $\operatorname{vecEmpty}$.
ModularGroup.TdefMathlib.LinearAlgebra.Matrix.SpecialLinearGroup, function or constantEnglish
$\operatorname{T}$ is a special linear group of $\mathrm{Fin}$ applied to $2$ and $\Integer$ defined as $\operatorname{of}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{vecCons}$ applied to $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{vecEmpty}$.
Matrix.stdBasisdefMathlib.LinearAlgebra.Matrix.StdBasis, function or constantWording
the standard basis of R (from the docstring)
English
Let $R$, $m$ and $n$ be sets. Then the standard basis of $R$ is a basis of $R$ and the set of matrixes of $n$ and $R$ defined as the map of the reindexing of the basis of the function that maps $x_{2}$ to the basis function of $R$ and $n$ and the sigma equivalence product of $m$ and $n$ and the matrix of $R$.
Module.Basis.matrixdefMathlib.LinearAlgebra.Matrix.StdBasis, function or constantWording
the matrix of b (from the name)
English
Let $m$ and $n$ be sets. Let $b$ be a basis of $R$ and $M$. Then the matrix of $b$ is a basis of $R$ and the set of matrixes of $n$ and $M$ defined as the map of the reindexing of the basis of the function that maps $x_{6}$ to the basis of the function that maps $x_{7}$ to $b$ and the composition of the sigma equivalence product of $m$ and $\Sigma$ applied to the function that maps $j$ to $x$ and the product congruence of the identity of $m$ and the sigma equivalence product of $n$ and $x$ and the matrix of $R$.
Matrix.colStochasticdefMathlib.LinearAlgebra.Matrix.Stochastic, function or constantEnglish
Let $R$ and $n$ be sets. Then $\operatorname{colStochastic}$ applied to $R$ and $n$ is a submonoid of the set of matrixes of $n$ and $R$.
Matrix.rowStochasticdefMathlib.LinearAlgebra.Matrix.Stochastic, function or constantEnglish
Let $R$ and $n$ be sets. Then $\operatorname{rowStochastic}$ applied to $R$ and $n$ is a submonoid of the set of matrixes of $n$ and $R$.
Matrix.GeneralLinearGroup.swapdefMathlib.LinearAlgebra.Matrix.Swap, function or constantWording
the swap of i and j (from the name)
English
Let $R$ be a set. Let $i$ and $j$ be elements of $n$. Then the swap of $i$ and $j$ is a general linear group of $n$ and $R$.
Matrix.swapdefMathlib.LinearAlgebra.Matrix.Swap, function or constantWording
the swap of i and j (from the name)
English
Let $R$ be a set. Let $i$ and $j$ be elements of $n$. Then the swap of $i$ and $j$ is a matrix of $n$ and $R$ defined as the permutation matrix of $R$ and the swap of $i$ and $j$.
Matrix.IsSymmdefMathlib.LinearAlgebra.Matrix.Symmetric, predicateWording
A is inverse (from the name)
English
Let $A$ be a matrix of $n$ and $x$. Then $A$ is inverse, if the transpose of $A$ is equal to $A$.
Algebra.leftMulMatrixdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix corresponding to the linear map of b (from the docstring)
English
Let $b$ be a basis of $R$ and $S$. Then the matrix corresponding to the linear map of $b$ is an algebra homomorphism of $S$ and the set of matrixes of $m$ and $R$.
LinearMap.toMatrixdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix of x9 and x10 (from the name)
English
Let $x_{9}$ be a basis of $R$ and $x_{3}$. Let $x_{10}$ be a basis of $R$ and $x_{4}$. Then the matrix of $x_{9}$ and $x_{10}$ is a linear equivalence of the set of linear maps of $x_{3}$ and $x_{4}$ and the set of matrixes of $n$ and $R$ defined as the composition of the arrow congruence of the equivalence function of $x_{9}$ and the equivalence function of $x_{10}$ and the matrix.
LinearMap.toMatrix'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix (from the name)
English
The matrix is a linear equivalence of the set of linear maps of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $m$ to elements of $R$ and the set of matrixes of $n$ and $R$.
LinearMap.toMatrixAlgEquivdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix algebra isomorphism of x6 (from the name)
English
Let $x_{6}$ be a basis of $R$ and $x_{3}$. Then the matrix algebra isomorphism of $x_{6}$ is an algebra isomorphism of the set of linear maps of $x_{3}$ and $x_{3}$ and the set of matrixes of $n$ and $R$ defined as the algebra isomorphism of the matrix of $x_{6}$ and $x_{6}$.
LinearMap.toMatrixAlgEquiv'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix algebra isomorphism (from the name)
English
The matrix algebra isomorphism is an algebra isomorphism of the set of linear maps of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ and the set of matrixes of $n$ and $R$ defined as the algebra isomorphism of the matrix.
LinearMap.toMatrixRight'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the right matrix (from the name)
English
The right matrix is a linear equivalence of the set of linear maps of the set of functions from elements of $m$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ and the set of matrixes of $n$ and $R$.
Matrix.mulVecBilindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the multiplicative vector bilinear of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the multiplicative vector bilinear of $R$ and $S$ is a linear map of the set of matrixes of $n$ and $A$ and the set of linear maps of the set of functions from elements of $n$ to elements of $A$ and the set of functions from elements of $m$ to elements of $A$.
Matrix.mulVecLindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
Let $M$ be a matrix of $n$ and $R$. Then $\operatorname{mulVecLin}$ applied to $M$ is a linear map of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $m$ to elements of $R$ defined as $\operatorname{mulVecBilin}$ applied to $R$, $R$ and $M$.
Matrix.toLindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
Let $x_{9}$ be a basis of $R$ and $x_{3}$. Let $x_{10}$ be a basis of $R$ and $x_{4}$. Then $\operatorname{toLin}$ applied to $x_{9}$ and $x_{10}$ is a linear equivalence of the set of matrixes of $n$ and $R$ and the set of linear maps of $x_{3}$ and $x_{4}$ defined as the inverse of the matrix of $x_{9}$ and $x_{10}$.
Matrix.toLin'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
$\operatorname{toLin'}$ is a linear equivalence of the set of matrixes of $n$ and $R$ and the set of linear maps of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $m$ to elements of $R$ defined as the inverse of the matrix.
Matrix.toLin'OfInvdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
Assume that $\EqtMACRoH {M \times \mathrm{M'}}{1}$. Assume that $\EqtMACRoH {\mathrm{M'} \times M}{1}$. Then $\operatorname{toLin'OfInv}$ applied to $\mathrm{hMM'}$ and $\mathrm{hM'M}$ is a linear equivalence of the set of functions from elements of $m$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$.
Matrix.toLinAlgEquivdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the linear algebra isomorphism of x6 (from the name)
English
Let $x_{6}$ be a basis of $R$ and $x_{3}$. Then the linear algebra isomorphism of $x_{6}$ is an algebra isomorphism of the set of matrixes of $n$ and $R$ and the set of linear maps of $x_{3}$ and $x_{3}$ defined as the inverse of the matrix algebra isomorphism of $x_{6}$.
Matrix.toLinAlgEquiv'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the linear algebra isomorphism (from the name)
English
The linear algebra isomorphism is an algebra isomorphism of the set of matrixes of $n$ and $R$ and the set of linear maps of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ defined as the inverse of the matrix algebra isomorphism.
Matrix.toLinOfInvdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
Let $x_{9}$ be a basis of $R$ and $x_{3}$. Let $x_{10}$ be a basis of $R$ and $x_{4}$. Assume that $\EqtMACRoH {M \times \mathrm{M'}}{1}$. Assume that $\EqtMACRoH {\mathrm{M'} \times M}{1}$. Then $\operatorname{toLinOfInv}$ applied to $x_{9}$, $x_{10}$, $\mathrm{hMM'}$ and $\mathrm{hM'M}$ is a linear equivalence of $x_{3}$ and $x_{4}$.
Matrix.toLinearEquivRight'OfInvdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the right linear equivalence of #1 and #2 (from the name)
English
Assume that $\EqtMACRoH {M \times \mathrm{M'}}{1}$. Assume that $\EqtMACRoH {\mathrm{M'} \times M}{1}$. Then the right linear equivalence of $\mathrm{hMM'}$ and $\mathrm{hM'M}$ is a linear equivalence of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $m$ to elements of $R$.
Matrix.toLinearMapRight'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the right linear map (from the name)
English
The right linear map is a linear equivalence of the set of matrixes of $n$ and $R$ and the set of linear maps of the set of functions from elements of $m$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ defined as the inverse of the right matrix.
Matrix.vecMulBilindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the vector multiplicative bilinear of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the vector multiplicative bilinear of $R$ and $S$ is a linear map of the set of functions from elements of $m$ to elements of $A$ and the set of linear maps of the set of matrixes of $n$ and $A$ and the set of functions from elements of $n$ to elements of $A$.
Matrix.vecMulLineardefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the linear map of M (from the docstring)
English
Let $M$ be a matrix of $n$ and $R$. Then the linear map of $M$ is a linear map of the set of functions from elements of $m$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ defined as $\operatorname{flip}$ applied to the vector multiplicative bilinear of $R$ and the set of multiplicative opposites of $R$ and $M$.
Module.Basis.enddefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the standard basis of the endomorphism algebra of b (from the docstring)
English
Let $b$ be a basis of $R$ and $M$. Then the standard basis of the endomorphism algebra of $b$ is a basis of $R$ and the set of ends of $R$ and $M$ defined as the linear map of $b$ and $b$.
Module.Basis.linearMapdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the linear map of x12 and x13 (from the name)
English
Let $x_{12}$ be a basis of $R$ and $x$. Let $x_{13}$ be a basis of $R$ and $x_{1}$. Then the linear map of $x_{12}$ and $x_{13}$ is a basis of $R$ and the set of linear maps of $x$ and $x_{1}$ defined as the map of the standard basis of $R$ and the inverse of the matrix of $x_{12}$ and $x_{13}$.
algEquivMatrixdefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the algebra isomorphism matrix of h (from the name)
English
Let $h$ be a basis of $R$ and $M$. Then the algebra isomorphism matrix of $h$ is an algebra isomorphism of the set of ends of $R$ and $M$ and the set of matrixes of $n$ and $R$ defined as the composition of the conjugate algebra isomorphism of $R$ and the equivalence function of $h$ and the algebra isomorphism matrix.
algEquivMatrix'defMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the algebra isomorphism matrix (from the name)
English
The algebra isomorphism matrix is an algebra isomorphism of the set of ends of $R$ and the set of functions from elements of $n$ to elements of $R$ and the set of matrixes of $n$ and $R$ defined as the matrix algebra isomorphism.
dotProductBilindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantEnglish
Let $R$ and $S$ be sets. Then $\mathrm{dotProductBilin}$ applied to $R$ and $S$ is a linear map of the set of functions from elements of $m$ to elements of $A$ and the set of linear maps of the set of functions from elements of $m$ to elements of $A$ and $A$.
endVecAlgEquivMatrixEnddefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the end vector algebra isomorphism matrix end of A and M (from the name)
English
Let $x$, $R$, $A$ and $M$ be sets. Then the end vector algebra isomorphism matrix end of $A$ and $M$ is an algebra isomorphism of the set of ends of $A$ and the set of functions from elements of $x$ to elements of $M$ and the set of matrixes of $x$ and the set of ends of $A$ and $M$.
endVecRingEquivMatrixEnddefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the end vector ring isomorphism matrix end of A and M (from the name)
English
Let $x$, $A$ and $M$ be sets. Then the end vector ring isomorphism matrix end of $A$ and $M$ is a ring isomorphism of the set of ends of $A$ and the set of functions from elements of $x$ to elements of $M$ and the set of matrixes of $x$ and the set of ends of $A$ and $M$.
matrixAlgEquivEndVecMulOppositedefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix algebra isomorphism end vector multiplicative opposite of R (from the name)
English
Let $R$ be a set. Then the matrix algebra isomorphism end vector multiplicative opposite of $R$ is an algebra isomorphism of the set of matrixes of $x$ and $A$ and the set of multiplicative opposites of the set of ends of $A$ and the set of functions from elements of $x$ to elements of $A$ defined as the composition of the opposite opposite of $R$ and the set of matrixes of $x$ and $A$ and $\operatorname{op}$ applied to the composition of the inverse of $\operatorname{mopMatrix}$ and the composition of the map matrix of the module end self of $R$ and the inverse of the end vector algebra isomorphism matrix end of $A$ and $A$.
matrixRingEquivEndVecMulOppositedefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the matrix ring isomorphism end vector multiplicative opposite (from the name)
English
The matrix ring isomorphism end vector multiplicative opposite is a ring isomorphism of the set of matrixes of $x$ and $A$ and the set of multiplicative opposites of the set of ends of $A$ and the set of functions from elements of $x$ to elements of $A$ defined as the ring isomorphism of the matrix algebra isomorphism end vector multiplicative opposite of $\Natural$.
vecMulVecBilindefMathlib.LinearAlgebra.Matrix.ToLin, function or constantWording
the vector multiplicative vector bilinear of R and S (from the name)
English
Let $R$ and $S$ be sets. Then the vector multiplicative vector bilinear of $R$ and $S$ is a linear map of the set of functions from elements of $m$ to elements of $A$ and the set of linear maps of the set of functions from elements of $n$ to elements of $A$ and the set of matrixes of $n$ and $A$.
Matrix.toLinearEquivdefMathlib.LinearAlgebra.Matrix.ToLinearEquiv, function or constantWording
the linear equivalence of b and A (from the name)
English
Let $b$ be a basis of $R$ and $M$. Let $A$ be a matrix of $n$ and $R$ such that the determinant of $A$ is a unit. Then the linear equivalence of $b$ and $A$ is a linear equivalence of $M$ and $M$.
Matrix.toLinearEquiv'defMathlib.LinearAlgebra.Matrix.ToLinearEquiv, function or constantWording
the linear equivalence of P and x3 (from the name)
English
Let $P$ be an invertible matrix of $n$ and $R$. Then the linear equivalence of $P$ and $x_{3}$ is a linear equivalence of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$ defined as $\operatorname{generalLinearEquiv}$ applied to $R$, the set of functions from elements of $n$ to elements of $R$ and $\operatorname{toLin}$ applied to the unit of $P$.
Matrix.tracedefMathlib.LinearAlgebra.Matrix.Trace, function or constantWording
the trace of A (from the docstring)
English
Let $A$ be a matrix of $n$ and $R$. Then the trace of $A$ is an element of $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{diag} (A , i)}$.
Matrix.traceAddMonoidHomdefMathlib.LinearAlgebra.Matrix.Trace, function or constantWording
the trace additive monoid homomorphism of n and R (from the name)
English
Let $n$ and $R$ be sets. Then the trace additive monoid homomorphism of $n$ and $R$ is an additive monoid homomorphism of the set of matrixes of $n$ and $R$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{trace}$ and $\mathrm{Matrix\_\_trace\_zero}$ applied to $n$ and $R$ and $\mathrm{Matrix\_\_trace\_add}$.
Matrix.traceLinearMapdefMathlib.LinearAlgebra.Matrix.Trace, function or constantWording
the trace linear map of x and R (from the name)
English
Let $n$, $x$ and $R$ be sets. Then the trace linear map of $x$ and $R$ is a linear map of the set of matrixes of $n$ and $R$ and $R$.
Matrix.Pivot.listTransvecColdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantEnglish
Let $M$ be a matrix of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Unit}$ and $x$. Then $\operatorname{listTransvecCol}$ applied to $M$ is a list of matrixes of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Unit}$ and $x$ defined as $\operatorname{ofFn}$ applied to the function that maps $i$ to the transvection of $\operatorname{inr}$ applied to $\operatorname{unit}$ and $\frac{ \operatorname{neg} (M (\operatorname{inl} (i), \operatorname{inr} (\operatorname{unit})))}{M (\operatorname{inr} (\operatorname{unit}), \operatorname{inr} (\operatorname{unit}))}$.
Matrix.Pivot.listTransvecRowdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantEnglish
Let $M$ be a matrix of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Unit}$ and $x$. Then $\operatorname{listTransvecRow}$ applied to $M$ is a list of matrixes of $\mathrm{Sum}$ applied to $\mathrm{Fin}$ applied to $r$ and $\mathrm{Unit}$ and $x$ defined as $\operatorname{ofFn}$ applied to the function that maps $i$ to the transvection of $\operatorname{inl}$ applied to $i$ and $\frac{ \operatorname{neg} (M (\operatorname{inr} (\operatorname{unit}), \operatorname{inl} (i)))}{M (\operatorname{inr} (\operatorname{unit}), \operatorname{inr} (\operatorname{unit}))}$.
Matrix.TransvectionStructstructureMathlib.LinearAlgebra.Matrix.Transvection, typeEnglish
Let $n$ and $R$ be sets. Then the elements of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$ are a basic type.
Matrix.TransvectionStruct.cdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then $\operatorname{c}$ applied to $\mathrm{self}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
Matrix.TransvectionStruct.idefMathlib.LinearAlgebra.Matrix.Transvection, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then $\operatorname{i}$ applied to $\mathrm{self}$ is an element of $n$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Matrix.TransvectionStruct.invdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantWording
the inverse of t (from the docstring)
English
Let $t$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then the inverse of $t$ is an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{i}$ applied to $t$, $\operatorname{j}$ applied to $t$, $\operatorname{hij}$ applied to $t$ and $\operatorname{neg}$ applied to $\operatorname{c}$ applied to $t$.
Matrix.TransvectionStruct.jdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantEnglish
Let $\mathrm{self}$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then $\operatorname{j}$ applied to $\mathrm{self}$ is an element of $n$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
Matrix.TransvectionStruct.reindexEquivdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantWording
the reindexing equivalence of e and t (from the name)
English
Let $e$ be an equivalence from $n$ to $p$. Let $t$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then the reindexing equivalence of $e$ and $t$ is an element of $\operatorname{TransvectionStruct}$ applied to $p$ and $R$.
Matrix.TransvectionStruct.sumInldefMathlib.LinearAlgebra.Matrix.Transvection, function or constantWording
the sum left injection of p and t (from the name)
English
Let $p$ be a set. Let $t$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then the sum left injection of $p$ and $t$ is an element of $\operatorname{TransvectionStruct}$ applied to $\mathrm{Sum}$ applied to $n$ and $p$ and $R$.
Matrix.TransvectionStruct.toMatrixdefMathlib.LinearAlgebra.Matrix.Transvection, function or constantWording
the matrix of t (from the name)
English
Let $t$ be an element of $\operatorname{TransvectionStruct}$ applied to $n$ and $R$. Then the matrix of $t$ is a matrix of $n$ and $R$ defined as the transvection of $\operatorname{j}$ applied to $t$ and $\operatorname{c}$ applied to $t$.
Matrix.transvectiondefMathlib.LinearAlgebra.Matrix.Transvection, function or constantWording
the transvection of j and c (from the name)
English
Let $i$ and $j$ be elements of $n$. Let $c$ be an element of $R$. Then the transvection of $j$ and $c$ is a matrix of $n$ and $R$ defined as $1 + \operatorname{single} (i , j , c)$.
Matrix.uniqueAddEquivdefMathlib.LinearAlgebra.Matrix.Unique, function or constantWording
the unique additive equivalence (from the name)
English
The unique additive equivalence is an additive equivalence of the set of matrixes of $n$ and $A$ and $A$.
Matrix.uniqueAlgEquivdefMathlib.LinearAlgebra.Matrix.Unique, function or constantWording
the unique algebra isomorphism (from the name)
English
The unique algebra isomorphism is an algebra isomorphism of the set of matrixes of $m$ and $A$ and $A$.
Matrix.uniqueEquivdefMathlib.LinearAlgebra.Matrix.Unique, function or constantWording
the unique equivalence (from the name)
English
The unique equivalence is an equivalence from the set of matrixes of $n$ and $A$ to $A$.
Matrix.uniqueLinearEquivdefMathlib.LinearAlgebra.Matrix.Unique, function or constantWording
the unique linear equivalence (from the name)
English
The unique linear equivalence is a linear equivalence of the set of matrixes of $n$ and $A$ and $A$.
Matrix.uniqueRingEquivdefMathlib.LinearAlgebra.Matrix.Unique, function or constantWording
the unique ring isomorphism (from the name)
English
The unique ring isomorphism is a ring isomorphism of the set of matrixes of $m$ and $A$ and $A$.
Matrix.vecdefMathlib.LinearAlgebra.Matrix.Vec, function or constantWording
the vector of A and x (from the name)
English
Let $A$ be a matrix of $n$ and $R$. Let $x$ be an element of $\mathrm{Prod}$ applied to $n$ and $m$. Then the vector of $A$ and $x$ is an element of $R$ defined as $A$ applied to $\ProdsndMACRoAA {x}$ and $\ProdfstMACRoZ {x}$.
WithConv.matrixToLin'StarAlgEquivdefMathlib.LinearAlgebra.Matrix.WithConv, function or constantWording
the matrix to linear star algebra isomorphism of n and x (from the name)
English
Let $m$, $n$ and $x$ be sets. Then the matrix to linear star algebra isomorphism of $n$ and $x$ is a star algebra isomorphism of $\mathrm{WithConv}$ applied to the set of matrixes of $n$ and $x$ and $\mathrm{WithConv}$ applied to the set of linear maps of the set of functions from elements of $n$ to elements of $x$ and the set of functions from elements of $m$ to elements of $x$.
LinearEquiv.multilinearMapCongrLeftdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the left multilinear map congruence of e (from the name)
English
Let $e$ be a function from elements $i$ of $x$ to linear equivalences of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$. Then the left multilinear map congruence of $i$ is a linear equivalence of the set of multilinear maps of $x_{2}$ and $x_{3}$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
LinearEquiv.multilinearMapCongrRightdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the right multilinear map congruence of S and g (from the name)
English
Let $S$ be a set. Let $g$ be a linear equivalence of $x_{2}$ and $x_{3}$. Then the right multilinear map congruence of $S$ and $g$ is a linear equivalence of the set of multilinear maps of $x_{1}$ and $x_{2}$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
LinearMap.compMultilinearMapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the composition multilinear map of g and f (from the name)
English
Let $g$ be a linear map of $x_{2}$ and $x_{3}$. Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Then the composition multilinear map of $g$ and $f$ is a multilinear map of $x_{1}$ and $x_{3}$.
LinearMap.compMultilinearMapₗdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the composition multilinear map of S and g (from the name)
English
Let $S$ be a set. Let $g$ be a linear map of $x_{2}$ and $x_{3}$. Then the composition multilinear map of $S$ and $g$ is a linear map of the set of multilinear maps of $x_{1}$ and $x_{2}$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
MultilinearMapstructureMathlib.LinearAlgebra.Multilinear.Basic, typeWording
multilinear map of x1 and x2 (from the name)
English
Let $R$ and $x_{2}$ be sets. Let $x_{1}$ be a function from elements of $x$ to sets. Then the multilinear maps of $x_{1}$ and $x_{2}$ are a basic type.
MultilinearMap.codRestrictdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $p$ be a submodule of $R$ and $x_{2}$ such that for all functions $v$ from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$, $\MembershipmemMACRoT {p}{f (v)}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $h$ is a multilinear map of $x_{1}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {p}{x_{8}})}$.
MultilinearMap.compLinearMapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the composition linear map of g and f (from the name)
English
Let $g$ be a multilinear map of $x_{2}$ and $x_{3}$. Let $f$ be a function from elements $i$ of $x$ to linear maps of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$. Then the composition linear map of $g$ and $i$ is a multilinear map of $x_{1}$ and $x_{3}$.
MultilinearMap.compLinearMapMultilineardefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
$\operatorname{compLinearMapMultilinear}$ is a multilinear map of the function that maps $i$ to the set of linear maps of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$ and the set of linear maps of the set of multilinear maps of $x_{2}$ and $x_{3}$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
MultilinearMap.compLinearMapₗdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the composition linear map of f (from the name)
English
Let $f$ be a function from elements $i$ of $x$ to linear maps of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$. Then the composition linear map of $i$ is a linear map of the set of multilinear maps of $x_{2}$ and $x_{3}$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
MultilinearMap.compMultilinearMapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the composition multilinear map of g and f (from the name)
English
Let $g$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $f$ be a function from elements $i$ of $x$ to multilinear maps of $N$ applied to $i$ and $x_{1}$ applied to $i$. Then the composition multilinear map of $g$ and $i$ is a multilinear map of the function that maps $j$ to $N$ applied to $\operatorname{fst}$ applied to $j$ and $\operatorname{snd}$ applied to $j$ and $x_{2}$.
MultilinearMap.constLinearEquivOfIsEmptydefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the constant linear equivalence of x1 (from the name)
English
Let $R$, $S$ and $x_{2}$ be sets. Let $x_{1}$ be a function from elements of $x$ to sets. Then the constant linear equivalence of $x_{1}$ is a linear equivalence of $x_{2}$ and the set of multilinear maps of $x_{1}$ and $x_{2}$.
MultilinearMap.constOfIsEmptydefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the constant of x1 and m (from the name)
English
Let $R$ be a set. Let $x_{1}$ be a function from elements of $x$ to sets. Let $m$ be an element of $x_{2}$. Then the constant of $x_{1}$ and $m$ is a multilinear map of $x_{1}$ and $x_{2}$.
MultilinearMap.domDomCongrdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the domain domain congruence of x9 and m (from the name)
English
Let $x_{9}$ be an equivalence from $x_{7}$ to $x_{8}$. Let $m$ be a multilinear map of the function that maps $x_{11}$ to $x$ and $x_{1}$. Then the domain domain congruence of $x_{9}$ and $m$ is a multilinear map of the function that maps $x_{10}$ to $x$ and $x_{1}$.
MultilinearMap.domDomCongrEquivdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the domain domain congruence equivalence of x9 (from the name)
English
Let $x_{9}$ be an equivalence from $x_{7}$ to $x_{8}$. Then the domain domain congruence equivalence of $x_{9}$ is an additive equivalence of the set of multilinear maps of the function that maps $x_{10}$ to $x$ and $x_{1}$ and the set of multilinear maps of the function that maps $x_{11}$ to $x$ and $x_{1}$.
MultilinearMap.domDomCongrLinearEquivdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the domain domain congruence linear equivalence of x11 (from the name)
English
Let $R$, $S$, $x$ and $x_{1}$ be sets. Let $x_{11}$ be an equivalence from $x_{9}$ to $x_{10}$. Then the domain domain congruence linear equivalence of $x_{11}$ is a linear equivalence of the set of multilinear maps of the function that maps $x_{12}$ to $x$ and $x_{1}$ and the set of multilinear maps of the function that maps $x_{13}$ to $x$ and $x_{1}$.
MultilinearMap.domDomCongrLinearEquiv'defMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the domain domain congruence linear equivalence of x1 and x11 (from the name)
English
Let $R$, $S$ and $x_{2}$ be sets. Let $x_{1}$ be a function from elements of $x$ to sets. Let $x_{11}$ be an equivalence from $x$ to $x_{10}$. Then the domain domain congruence linear equivalence of $x_{1}$ and $x_{11}$ is a linear equivalence of the set of multilinear maps of $x_{1}$ and $x_{2}$ and the set of multilinear maps of the function that maps $i$ to $x_{1}$ applied to $\operatorname{symm}$ applied to $x_{11}$ and $i$ and $x_{2}$.
MultilinearMap.domDomRestrictdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $P$ be a function from elements of $x$ to propositions. Let $z$ be a function from elements $i_{1}$ of $\SubtypeSet {a}{\mathrm{not} (P (a))}$ to elements of $x_{1}$ applied to $i_{1}$. Then $\operatorname{domDomRestrict}$ applied to $f$, $P$, $i_{1}$ and $z$ is a multilinear map of the function that maps $i$ to $x_{1}$ applied to $i$ and $x_{2}$.
MultilinearMap.domDomRestrictₗdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $P$ be a function from elements of $x$ to propositions. Then $\mathrm{MultilinearMap\_\_domDomRestrict\_u2097\_}$ applied to $f$ and $P$ is a multilinear map of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of multilinear maps of the function that maps $i_{1}$ to $x_{1}$ applied to $i_{1}$ and $x_{2}$.
MultilinearMap.iteratedFDerivdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the iterated derivative of k and x9 (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $k$ be an element of $\Natural$. Let $x_{9}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Then the iterated derivative of $k$ and $i_{1}$ is a multilinear map of the function that maps $x_{10}$ to the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $x_{2}$ defined as the function that maps $x_{9}$ to $\FinsetSum {\FinsetunivMACRoAC}{e}{\operatorname{iteratedFDerivComponent} (f , \operatorname{toEquivRange} (e), \lambda i_{2} . i_{1} (i_{2}))}{x_{9}}$.
MultilinearMap.iteratedFDerivComponentdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the iterated derivative component of f and e (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $e$ be an equivalence from $x_{8}$ to the set of elements of $s$. Then the iterated derivative component of $f$ and $e$ is a multilinear map of the function that maps $i$ to $x_{1}$ applied to $i$ and the set of multilinear maps of the function that maps $x_{10}$ to the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ and $x_{2}$.
MultilinearMap.linearDerivdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the linear derivative of f and x10 (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $x_{10}$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Then the linear derivative of $f$ and $i_{1}$ is a linear map of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $x_{2}$ defined as the function that maps $x_{10}$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{toLinearMap} (i_{1} , i), \operatorname{proj} (i))}{x_{10}}$.
MultilinearMap.mapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the map of f and p (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $p$ be a function from elements $i$ of $x$ to submodules of $R$ and $x_{1}$ applied to $i$. Then the map of $f$ and $i$ is a difference multiplicative action of $R$ and $x_{2}$.
MultilinearMap.mk'defMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $f$ be a function from functions from elements $i_{4}$ of $x$ to elements of $x_{1}$ applied to $i_{4}$ to elements of $x_{2}$ such that $\mathrm{autoParam}$ holds for the proposition that for all functions $m_{1}$ from elements $i_{3}$ of $x$ to elements of $x_{1}$ applied to $i_{3}$, for all elements $i_{2}$ of $x$, for all elements $x_{10}$ of $x_{1}$ applied to $i_{2}$, for all elements $y$ of $x_{1}$ applied to $i_{2}$, $\EqtMACRoH {f (\operatorname{update} (m_{1} , i_{2} , x_{10} + y))}{f (\operatorname{update} (m_{1} , i_{2} , x_{10}))+ f (\operatorname{update} (m_{1} , i_{2} , y))}$ and $\mathrm{MultilinearMap\_\_mk'\_\_\_auto\_1}$ and $\mathrm{autoParam}$ holds for the proposition that for all functions $m$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$, for all elements $i$ of $x$, for all elements $c$ of $R$, for all elements $x_{9}$ of $x_{1}$ applied to $i$, $\EqtMACRoH {f (\operatorname{update} (m , i , \HSMulhSMulMACRoAL {c}{x_{9}}))}{\HSMulhSMulMACRoAL {c}{f (\operatorname{update} (m , i , x_{9}))}}$ and $\mathrm{MultilinearMap\_\_mk'\_\_\_auto\_3}$. Then $\operatorname{mk'}$ applied to $f$, $h$ and $h_{1}$ is a multilinear map of $x_{1}$ and $x_{2}$.
MultilinearMap.mkPiAlgebradefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product algebra of x and A (from the name)
English
Let $R$, $x$ and $A$ be sets. Then the product algebra of $x$ and $A$ is a multilinear map of the function that maps $x_{5}$ to $A$ and $A$.
MultilinearMap.mkPiAlgebraFindefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $R$ and $A$ be sets. Let $n$ be a natural number. Then $\operatorname{mkPiAlgebraFin}$ applied to $R$, $n$ and $A$ is a multilinear map of the function that maps $x_{3}$ to $A$ and $A$.
MultilinearMap.mkPiRingdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product ring of z (from the name)
English
Let $R$ and $x$ be sets. Let $z$ be an element of $x_{1}$. Then the product ring of $z$ is a multilinear map of the function that maps $x_{6}$ to $R$ and $x_{1}$ defined as the right scalar multiple of the product algebra of $x$ and $R$ and $z$.
MultilinearMap.ofSubsingletondefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the multilinear map of i (from the name)
English
Let $R$, $x_{1}$ and $x_{2}$ be sets. Let $i$ be an element of $x$. Then the multilinear map of $i$ is an equivalence from the set of linear maps of $x_{1}$ and $x_{2}$ to the set of multilinear maps of the function that maps $x_{8}$ to $x_{1}$ and $x_{2}$.
MultilinearMap.ofSubsingletonₗdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the multilinear map of i (from the name)
English
Let $R$, $S$, $x_{1}$ and $x_{2}$ be sets. Let $i$ be an element of $x$. Then the multilinear map of $i$ is a linear equivalence of the set of linear maps of $x_{1}$ and $x_{2}$ and the set of multilinear maps of the function that maps $x_{10}$ to $x_{1}$ and $x_{2}$.
MultilinearMap.pidefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product of f (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $x_{5}$ to multilinear maps of $x_{1}$ and $\mathrm{M'}$ applied to $i_{1}$. Then the product of $i_{1}$ is a multilinear map of $x_{1}$ and the set of functions from elements $i$ of $x_{5}$ to elements of $\mathrm{M'}$ applied to $i$.
MultilinearMap.piLinearMapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product linear map (from the name)
English
The product linear map is a linear map of the set of multilinear maps of $x_{2}$ and $x_{3}$ and the set of multilinear maps of the function that maps $i$ to the set of linear maps of $x_{1}$ applied to $i$ and $x_{2}$ applied to $i$ and the set of multilinear maps of $x_{1}$ and $x_{3}$.
MultilinearMap.piRingEquivdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product ring isomorphism (from the name)
English
The product ring isomorphism is a linear equivalence of $x_{1}$ and the set of multilinear maps of the function that maps $x_{6}$ to $R$ and $x_{1}$.
MultilinearMap.proddefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the product of f and g (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $g$ be a multilinear map of $x_{1}$ and $x_{3}$. Then the product of $f$ and $g$ is a multilinear map of $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$.
MultilinearMap.rangedefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the range of f (from the docstring)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Then the range of $f$ is a difference multiplicative action of $R$ and $x_{2}$ defined as the map of $f$ and the function that maps $x_{8}$ to the top.
MultilinearMap.restrdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the restriction of s and z (from the name)
English
Let $f$ be a multilinear map of the function that maps $x_{7}$ to $\mathrm{M'}$ and $x$. Let $s$ be a finite set of $\mathrm{Fin}$ applied to $n$ such that $\FinsetcardMACRoM {s}= k$. Let $z$ be an element of $\mathrm{M'}$. Then the restriction of $s$ and $z$ is a multilinear map of the function that maps $x_{6}$ to $\mathrm{M'}$ and $x$.
MultilinearMap.restrictScalarsdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantEnglish
Let $R$ be a set. Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a multilinear map of $x_{1}$ and $x_{2}$.
MultilinearMap.smulRightdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the right scalar multiple of f and z (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $R$. Let $z$ be an element of $x_{2}$. Then the right scalar multiple of $f$ and $z$ is a multilinear map of $x_{1}$ and $x_{2}$ defined as the composition multilinear map of the right scalar multiple of the identity and $z$ and $f$.
MultilinearMap.toFundefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the underlying multivariate function of self and x8 (from the docstring)
English
Let $\mathrm{self}$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $x_{8}$ be a function from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$. Then the underlying multivariate function of $\mathrm{self}$ and $i$ is an element of $x_{2}$ defined as the function that maps $x_{8}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$, $i$ and $x_{8}$.
MultilinearMap.toLinearMapdefMathlib.LinearAlgebra.Multilinear.Basic, function or constantWording
the linear map of m and i1 (from the name)
English
Let $f$ be a multilinear map of $x_{1}$ and $x_{2}$. Let $m$ be a function from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$. Let $i$ be an element of $x$. Then the linear map of $i_{1}$ and $m$ is a linear map of $x_{1}$ applied to $i$ and $x_{2}$.
Basis.multilinearMapdefMathlib.LinearAlgebra.Multilinear.Basis, function or constantWording
the multilinear map of b and i1 (from the name)
English
Let $b$ be a function from elements $i_{1}$ of $x$ to bases of $R$ and $M$ applied to $i_{1}$. Let $\mathrm{b'}$ be a basis of $R$ and $N$. Then the multilinear map of $i_{1}$ and $b$ is a basis of $R$ and the set of multilinear maps of $M$ and $N$ defined as the function that maps $\mathrm{b'}$ to $\operatorname{ofRepr}$ applied to the composition of the composition of the left multilinear map congruence of the function that maps $i$ to the inverse of the representation of $i_{1}$ applied to $i$ and the right multilinear map congruence of $R$ and the representation of $b$ and the inverse of the free finitely supported function equivalence and $\mathrm{b'}$.
LinearMap.uncurryLeftdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantEnglish
Let $f$ be a linear map of $M$ applied to $0$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succ}$ applied to $i$ and $x$. Then $\operatorname{uncurryLeft}$ applied to $f$ is a multilinear map of $M$ and $x$.
LinearMap.uncurryMiddefMathlib.LinearAlgebra.Multilinear.Curry, function or constantEnglish
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a linear map of $M$ applied to $p$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $x$. Then $\operatorname{uncurryMid}$ applied to $p$ and $f$ is a multilinear map of $M$ and $x$.
MultilinearMap.curryFinFinsetdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the curry finite finite set of hl and #5 (from the name)
English
Let $R$, $x$ and $\mathrm{M'}$ be sets. Assume that $\FinsetcardMACRoM {s}= k$. Assume that the cardinality of the complement of $s$ is equal to $l$. Then the curry finite finite set of $\mathrm{hk}$ and $\mathrm{hl}$ is a linear equivalence of the set of multilinear maps of the function that maps $x_{6}$ to $\mathrm{M'}$ and $x$ and the set of multilinear maps of the function that maps $x_{7}$ to $\mathrm{M'}$ and the set of multilinear maps of the function that maps $x_{8}$ to $\mathrm{M'}$ and $x$ defined as the composition of the domain domain congruence linear equivalence of the inverse of the finite sum equivalence of $\mathrm{hk}$ and $\mathrm{hl}$ and the curry sum equivalence.
MultilinearMap.curryLeftdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the left curry of f (from the name)
English
Let $f$ be a multilinear map of $M$ and $x$. Then the left curry of $f$ is a linear map of $M$ applied to $0$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succ}$ applied to $i$ and $x$.
MultilinearMap.curryMiddefMathlib.LinearAlgebra.Multilinear.Curry, function or constantEnglish
Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Let $f$ be a multilinear map of $M$ and $x$. Then $\operatorname{curryMid}$ applied to $p$ and $f$ is a linear map of $M$ applied to $p$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $x$.
MultilinearMap.curryMidLinearEquivdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantEnglish
Let $R$ and $x$ be sets. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Let $p$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then $\operatorname{curryMidLinearEquiv}$ applied to $R$, $M$, $x$ and $p$ is a linear equivalence of the set of multilinear maps of $M$ and $x$ and the set of linear maps of $M$ applied to $p$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succAbove}$ applied to $p$ and $i$ and $x$.
MultilinearMap.curryRightdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the right curry of f (from the name)
English
Let $f$ be a multilinear map of $M$ and $x$. Then the right curry of $f$ is a multilinear map of the function that maps $i$ to $M$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of linear maps of $M$ applied to $\operatorname{last}$ applied to $n$ and $x$.
MultilinearMap.currySumdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the curry sum of f (from the name)
English
Let $f$ be a multilinear map of $N$ and $x_{2}$. Then the curry sum of $f$ is a multilinear map of the function that maps $i$ to $N$ applied to $\operatorname{inl}$ applied to $i$ and the set of multilinear maps of the function that maps $i_{1}$ to $N$ applied to $\operatorname{inr}$ applied to $i_{1}$ and $x_{2}$.
MultilinearMap.currySumEquivdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the curry sum equivalence (from the name)
English
The curry sum equivalence is a linear equivalence of the set of multilinear maps of $N$ and $x_{2}$ and the set of multilinear maps of the function that maps $i$ to $N$ applied to $\operatorname{inl}$ applied to $i$ and the set of multilinear maps of the function that maps $i_{1}$ to $N$ applied to $\operatorname{inr}$ applied to $i_{1}$ and $x_{2}$.
MultilinearMap.uncurryRightdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantEnglish
Let $f$ be a multilinear map of the function that maps $i$ to $M$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of linear maps of $M$ applied to $\operatorname{last}$ applied to $n$ and $x$. Then $\operatorname{uncurryRight}$ applied to $f$ is a multilinear map of $M$ and $x$.
MultilinearMap.uncurrySumdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the uncurrying sum of g (from the name)
English
Let $g$ be a multilinear map of the function that maps $i$ to $N$ applied to $\operatorname{inl}$ applied to $i$ and the set of multilinear maps of the function that maps $i_{1}$ to $N$ applied to $\operatorname{inr}$ applied to $i_{1}$ and $x_{2}$. Then the uncurrying sum of $g$ is a multilinear map of $N$ and $x_{2}$.
multilinearCurryLeftEquivdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the multilinear curry left equivalence of M (from the name)
English
Let $R$ and $x$ be sets. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then the multilinear curry left equivalence of $M$ is a linear equivalence of the set of multilinear maps of $M$ and $x$ and the set of linear maps of $M$ applied to $0$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{succ}$ applied to $i$ and $x$.
multilinearCurryRightEquivdefMathlib.LinearAlgebra.Multilinear.Curry, function or constantWording
the multilinear curry right equivalence of M (from the name)
English
Let $R$ and $x$ be sets. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then the multilinear curry right equivalence of $M$ is a linear equivalence of the set of multilinear maps of $M$ and $x$ and the set of multilinear maps of the function that maps $i$ to $M$ applied to $\operatorname{castSucc}$ applied to $i$ and the set of linear maps of $M$ applied to $\operatorname{last}$ applied to $n$ and $x$.
MultilinearMap.dfinsuppFamilydefMathlib.LinearAlgebra.Multilinear.DFinsupp, function or constantEnglish
Let $f$ be a function from functions $p$ from elements $i_{2}$ of $x$ to elements of $x_{1}$ applied to $i_{2}$ to multilinear maps of the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $p$ applied to $i_{1}$ and $N$ applied to $p$. Then $\operatorname{dfinsuppFamily}$ applied to $p$ and $f$ is a multilinear map of the function that maps $i$ to the set of finitely supported functions of the function that maps $j$ to $M$ applied to $i$ and $j$ and the set of finitely supported functions of the function that maps $t$ to $N$ applied to $t$.
MultilinearMap.dfinsuppFamilyₗdefMathlib.LinearAlgebra.Multilinear.DFinsupp, function or constantEnglish
$\mathrm{MultilinearMap\_\_dfinsuppFamily\_u2097\_}$ is a linear map of the set of functions from functions $p$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to multilinear maps of the function that maps $i$ to $M$ applied to $i$ and $p$ applied to $i$ and $N$ applied to $p$ and the set of multilinear maps of the function that maps $i_{2}$ to the set of finitely supported functions of the function that maps $j$ to $M$ applied to $i_{2}$ and $j$ and the set of finitely supported functions of the function that maps $t$ to $N$ applied to $t$.
MultilinearMap.freeDFinsuppEquivdefMathlib.LinearAlgebra.Multilinear.DFinsupp, function or constantWording
the free finitely supported function equivalence (from the name)
English
The free finitely supported function equivalence is a linear equivalence of the set of finitely supported functions of the function that maps $x_{8}$ to $R$ and the set of multilinear maps of the function that maps $i$ to the set of finitely supported functions of the function that maps $x_{9}$ to $R$ and the set of finitely supported functions of the function that maps $x_{10}$ to $R$ defined as the composition of the composition of the composition of the composition of the domain congruence of the inverse of the sigma equivalence product of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $x_{2}$ and the sigma curry equivalence and the linear equivalence function on finite type and the right product congruence of the function that maps $x_{8}$ to the product ring isomorphism and $\operatorname{fromDFinsuppEquiv}$ applied to $x_{1}$ and $R$.
MultilinearMap.fromDFinsuppEquivdefMathlib.LinearAlgebra.Multilinear.DFinsupp, function or constantEnglish
Let $x_{1}$ be a function from elements of $x$ to sets. Let $R$ be a set. Then $\operatorname{fromDFinsuppEquiv}$ applied to $x_{1}$ and $R$ is a linear equivalence of the set of functions from functions $p$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to multilinear maps of the function that maps $i$ to $M$ applied to $i$ and $p$ applied to $i$ and $N$ and the set of multilinear maps of the function that maps $i_{2}$ to the set of finitely supported functions of the function that maps $j$ to $M$ applied to $i_{2}$ and $j$ and $N$.
MultilinearMap.fromDirectSumEquivdefMathlib.LinearAlgebra.Multilinear.DirectSum, function or constantEnglish
$\operatorname{fromDirectSumEquiv}$ is a linear equivalence of the set of functions from functions $p$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to multilinear maps of the function that maps $i$ to $M$ applied to $i$ and $p$ applied to $i$ and $\mathrm{M'}$ and the set of multilinear maps of the function that maps $i_{2}$ to the set of direct sums of $x_{1}$ applied to $i_{2}$ and the function that maps $j$ to $M$ applied to $i_{2}$ and $j$ and $\mathrm{M'}$ defined as $\operatorname{fromDFinsuppEquiv}$ applied to $x_{1}$ and $R$.
MultilinearMap.freeFinsuppEquivdefMathlib.LinearAlgebra.Multilinear.Finsupp, function or constantWording
the free finitely supported function equivalence (from the name)
English
The free finitely supported function equivalence is a linear equivalence of $\FinsuppMACRoQ {\mathrm{Prod} (\mathrm{Elem} (x)\rightarrow x_{2} (i), x_{1})}{R}$ and the set of multilinear maps of the function that maps $i_{1}$ to $\FinsuppMACRoQ {x_{2} (i_{1})}{R}$ and $\FinsuppMACRoQ {x_{1}}{R}$ defined as the composition of the composition of the composition of the finitely supported function linear equivalence finitely supported function of $R$ and the free finitely supported function equivalence and the inverse of the right multilinear map congruence of $R$ and the finitely supported function linear equivalence finitely supported function of $R$ and the left multilinear map congruence of the function that maps $x_{10}$ to the finitely supported function linear equivalence finitely supported function of $R$.
MultilinearMap.piFamilydefMathlib.LinearAlgebra.Multilinear.Pi, function or constantWording
the product family of f (from the name)
English
Let $f$ be a function from functions $p$ from elements $i_{3}$ of $x$ to elements of $x_{1}$ applied to $i_{3}$ to multilinear maps of the function that maps $i_{2}$ to $M$ applied to $i_{2}$ and $p$ applied to $i_{2}$ and $N$ applied to $p$. Then the product family of $p$ is a multilinear map of the function that maps $i$ to the set of functions from elements $j$ of $x_{1}$ applied to $i$ to elements of $M$ applied to $i$ and $j$ and the set of functions from functions $t$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to elements of $N$ applied to $t$.
MultilinearMap.piFamilyₗdefMathlib.LinearAlgebra.Multilinear.Pi, function or constantWording
the product family (from the name)
English
The product family is a linear map of the set of functions from functions $p$ from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to multilinear maps of the function that maps $i$ to $M$ applied to $i$ and $p$ applied to $i$ and $N$ applied to $p$ and the set of multilinear maps of the function that maps $i_{2}$ to the set of functions from elements $j$ of $x_{1}$ applied to $i_{2}$ to elements of $M$ applied to $i_{2}$ and $j$ and the set of functions from functions $t$ from elements $i_{3}$ of $x$ to elements of $x_{1}$ applied to $i_{3}$ to elements of $N$ applied to $t$.
MultilinearMap.domCoproddefMathlib.LinearAlgebra.Multilinear.TensorProduct, function or constantWording
the domain coproduct of a and b (from the name)
English
Let $a$ be a multilinear map of the function that maps $x_{13}$ to $N$ and $x_{3}$. Let $b$ be a multilinear map of the function that maps $x_{12}$ to $N$ and $x_{6}$. Then the domain coproduct of $a$ and $b$ is a multilinear map of the function that maps $x_{11}$ to $N$ and the set of tensor products of $x_{3}$ and $x_{6}$ defined as $\operatorname{domCoprodDep}$ applied to $a$ and $b$.
MultilinearMap.domCoprod'defMathlib.LinearAlgebra.Multilinear.TensorProduct, function or constantWording
the domain coproduct (from the name)
English
The domain coproduct is a linear map of the set of tensor products of the set of multilinear maps of the function that maps $x_{11}$ to $N$ and $x_{3}$ and the set of multilinear maps of the function that maps $x_{12}$ to $N$ and $x_{6}$ and the set of multilinear maps of the function that maps $x_{13}$ to $N$ and the set of tensor products of $x_{3}$ and $x_{6}$ defined as $\operatorname{domCoprodDep'}$.
MultilinearMap.domCoprodDepdefMathlib.LinearAlgebra.Multilinear.TensorProduct, function or constantEnglish
Let $a$ be a multilinear map of the function that maps $x_{12}$ to $N$ applied to $\operatorname{inl}$ applied to $x_{12}$ and $x_{3}$. Let $b$ be a multilinear map of the function that maps $x_{11}$ to $N$ applied to $\operatorname{inr}$ applied to $x_{11}$ and $x_{6}$. Then $\operatorname{domCoprodDep}$ applied to $a$ and $b$ is a multilinear map of $N$ and the set of tensor products of $x_{3}$ and $x_{6}$.
MultilinearMap.domCoprodDep'defMathlib.LinearAlgebra.Multilinear.TensorProduct, function or constantEnglish
$\operatorname{domCoprodDep'}$ is a linear map of the set of tensor products of the set of multilinear maps of the function that maps $x_{11}$ to $N$ applied to $\operatorname{inl}$ applied to $x_{11}$ and $x_{3}$ and the set of multilinear maps of the function that maps $x_{12}$ to $N$ applied to $\operatorname{inr}$ applied to $x_{12}$ and $x_{6}$ and the set of multilinear maps of $N$ and the set of tensor products of $x_{3}$ and $x_{6}$.
Module.Basis.adjustToOrientationdefMathlib.LinearAlgebra.Orientation, function or constantEnglish
Let $e$ be a basis of $R$ and $M$. Let $x_{7}$ be an orientation of $M$ and $x_{4}$. Then $\operatorname{adjustToOrientation}$ applied to $e$ and $x_{7}$ is a basis of $R$ and $M$ defined as $\iteMACRoG {(\EqtMACRoH {\operatorname{orientation} (e)}{x_{7}})}{e}{\operatorname{unitsSMul} (e , \operatorname{update} (1 , \operatorname{arbitrary} (x_{4}), \operatorname{neg} (1)))}$.
Module.Basis.orientationdefMathlib.LinearAlgebra.Orientation, function or constantWording
the orientation of e (from the name)
English
Let $e$ be a basis of $R$ and $M$. Then the orientation of $e$ is an orientation of $M$ and $x_{4}$.
Module.OrientedclassMathlib.LinearAlgebra.Orientation, predicateEnglish
Let $R$, $M$ and $x_{4}$ be sets. Then we can say that $\operatorname{Oriented}$ holds for $R$, $M$ and $x_{4}$.
Module.Oriented.positiveOrientationdefMathlib.LinearAlgebra.Orientation, function or constantWording
the positive orientation (from the name)
English
The positive orientation is an orientation of $M$ and $x_{4}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
OrientationdefMathlib.LinearAlgebra.Orientation, typeWording
orientation of M and x4 (from the name)
English
Let $R$, $M$ and $x_{4}$ be sets. Then an orientation of $M$ and $x_{4}$ is an element of the function that maps $R$, $M$ and $x_{4}$ to the set of rays of $R$ and the set of alternating maps of $R$ and $x_{4}$.
Orientation.mapdefMathlib.LinearAlgebra.Orientation, function or constantWording
the map of x6 and e (from the name)
English
Let $x_{6}$ be a set. Let $e$ be a linear equivalence of $M$ and $N$. Then the map of $x_{6}$ and $e$ is an equivalence from the set of orientations of $M$ and $x_{6}$ to the set of orientations of $N$ and $x_{6}$ defined as the map of the domain congruence of $e$.
Orientation.reindexdefMathlib.LinearAlgebra.Orientation, function or constantWording
the reindexing of e (from the name)
English
Let $R$ and $M$ be sets. Let $e$ be an equivalence from $x_{4}$ to $x_{5}$. Then the reindexing of $e$ is an equivalence from the set of orientations of $M$ and $x_{4}$ to the set of orientations of $M$ and $x_{5}$ defined as the map of the domain domain congruence of $R$ and $e$.
Orientation.someBasisdefMathlib.LinearAlgebra.Orientation, function or constantEnglish
Let $x_{7}$ be an orientation of $M$ and $x_{4}$. Assume that the cardinality of $x_{4}$ is equal to the rank of $R$ and $M$. Then $\operatorname{someBasis}$ applied to $x_{7}$ and $h_{3}$ is a basis of $R$ and $M$ defined as $\operatorname{adjustToOrientation}$ applied to the reindexing of the finite basis of $R$ and $M$ and the inverse of $\operatorname{equivFinOfCardEq}$ applied to $h_{3}$ and $x_{7}$.
LinearEquiv.flipdefMathlib.LinearAlgebra.PerfectPairing.Basic, function or constantWording
the flip of e (from the name)
English
Let $e$ be a linear equivalence of $N$ and the set of duals of $R$ and $M$. Then the flip of $e$ is a linear equivalence of $M$ and the set of duals of $R$ and $N$ defined as the composition of the evaluation equivalence of $R$ and $M$ and the dual map of $e$.
LinearMap.IsPerfPairclassMathlib.LinearAlgebra.PerfectPairing.Basic, predicateEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Then we can say that $\operatorname{IsPerfPair}$ holds for $p$.
LinearMap.IsPerfectComplstructureMathlib.LinearAlgebra.PerfectPairing.Basic, predicateEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $U$ be a submodule of $R$ and $M$. Let $V$ be a submodule of $R$ and $N$. Then we can say that $\operatorname{IsPerfectCompl}$ holds for $p$, $U$ and $V$.
LinearMap.toPerfPairdefMathlib.LinearAlgebra.PerfectPairing.Basic, function or constantEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Then $\operatorname{toPerfPair}$ applied to $p$ is a linear equivalence of $M$ and the set of duals of $R$ and $N$.
Fin.consLinearEquivdefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $R$ be a set. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to the successor of $n$ to sets. Then $\operatorname{consLinearEquiv}$ applied to $R$ and $M$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ applied to $0$ and the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $n$ to elements of $M$ applied to $\operatorname{succ}$ applied to $i$ and the set of functions from elements $i_{1}$ of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $M$ applied to $i_{1}$.
Function.ExtendByZero.linearMapdefMathlib.LinearAlgebra.Pi, function or constantWording
the linear map of s (from the name)
English
Let $R$ and $M$ be sets. Let $s$ be a function from elements of $x$ to elements of $x_{1}$. Then the linear map of $s$ is a linear map of the set of functions from elements of $x$ to elements of $M$ and the set of functions from elements of $x_{1}$ to elements of $M$.
LinearEquiv.finTwoArrowdefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{finTwoArrow}$ applied to $R$ and $M$ is a linear equivalence of the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $M$ and $\mathrm{Prod}$ applied to $M$ and $M$.
LinearEquiv.funUniquedefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $x$, $R$ and $M$ be sets. Then $\operatorname{funUnique}$ applied to $x$, $R$ and $M$ is a linear equivalence of the set of functions from elements of $x$ to elements of $M$ and $M$.
LinearEquiv.linearMapPidefMathlib.LinearAlgebra.Pi, function or constantWording
the linear map product of S (from the name)
English
Let $S$ be a set. Then the linear map product of $S$ is a linear equivalence of the set of functions from elements $i$ of $x_{1}$ to linear maps of $x$ and $x_{5}$ applied to $i$ and the set of linear maps of $x$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $x_{5}$ applied to $i_{1}$.
LinearEquiv.piCongrLeftdefMathlib.LinearAlgebra.Pi, function or constantWording
the left product congruence of x3 and e (from the name)
English
Let $R$ be a set. Let $x_{3}$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x_{1}$ to $x$. Then the left product congruence of $x_{3}$ and $e$ is a linear equivalence of the set of functions from elements $\mathrm{i'}$ of $x_{1}$ to elements of $x_{3}$ applied to $e$ applied to $\mathrm{i'}$ and the set of functions from elements $i$ of $x$ to elements of $x_{3}$ applied to $i$ defined as the inverse of the left product congruence of $x_{3}$ and the inverse of $e$.
LinearEquiv.piCongrLeft'defMathlib.LinearAlgebra.Pi, function or constantWording
the left product congruence of x3 and e (from the name)
English
Let $R$ be a set. Let $x_{3}$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the left product congruence of $x_{3}$ and $e$ is a linear equivalence of the set of functions from elements $\mathrm{i'}$ of $x$ to elements of $x_{3}$ applied to $\mathrm{i'}$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{3}$ applied to $\operatorname{symm}$ applied to $e$ and $i$.
LinearEquiv.piCongrRightdefMathlib.LinearAlgebra.Pi, function or constantWording
the right product congruence of e (from the name)
English
Let $e$ be a function from elements $i_{2}$ of $x$ to linear equivalences of $x_{2}$ applied to $i_{2}$ and $x_{3}$ applied to $i_{2}$. Then the right product congruence of $i_{2}$ is a linear equivalence of the set of functions from elements $i$ of $x$ to elements of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{3}$ applied to $i_{1}$.
LinearEquiv.piCurrydefMathlib.LinearAlgebra.Pi, function or constantWording
the product curry of R and x3 (from the name)
English
Let $R$ be a set. Let $x_{3}$ be a function from elements $i_{2}$ of $x_{1}$ and elements of $x_{2}$ applied to $i_{2}$ to sets. Then the product curry of $R$ and $i_{2}$ is a linear equivalence of the set of functions from elements $i$ of $\Sigma$ applied to $x_{2}$ to elements of $x_{3}$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{1}$ and elements $j$ of $x_{2}$ applied to $i_{1}$ to elements of $x_{3}$ applied to $i_{1}$ and $j$.
LinearEquiv.piFinTwodefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $R$ be a set. Let $M$ be a function from elements of $\mathrm{Fin}$ applied to $2$ to sets. Then $\operatorname{piFinTwo}$ applied to $R$ and $M$ is a linear equivalence of the set of functions from elements $i$ of $\mathrm{Fin}$ applied to $2$ to elements of $M$ applied to $i$ and $\mathrm{Prod}$ applied to $M$ applied to $0$ and $M$ applied to $1$.
LinearEquiv.piOptionEquivProddefMathlib.LinearAlgebra.Pi, function or constantWording
the product option equivalence product of R (from the name)
English
Let $R$ be a set. Then the product option equivalence product of $R$ is a linear equivalence of the set of functions from elements $i$ of $\mathrm{Option}$ applied to $x_{1}$ to elements of $M$ applied to $i$ and $\mathrm{Prod}$ applied to $M$ applied to $\operatorname{none}$ and the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $M$ applied to $\operatorname{some}$ applied to $i_{1}$.
LinearEquiv.piRingdefMathlib.LinearAlgebra.Pi, function or constantWording
the product ring of x and S (from the name)
English
Let $R$, $M$, $x$ and $S$ be sets. Then the product ring of $x$ and $S$ is a linear equivalence of the set of linear maps of the set of functions from elements of $x$ to elements of $R$ and $M$ and the set of functions from elements of $x$ to elements of $M$ defined as the composition of the inverse of $\operatorname{lsum}$ applied to $R$, the function that maps $x_{8}$ to $R$ and $S$ and the right product congruence of the function that maps $x_{9}$ to $\operatorname{ringLmapEquivSelf}$ applied to $R$, $S$ and $M$.
LinearEquiv.sumArrowLequivProdArrowdefMathlib.LinearAlgebra.Pi, function or constantWording
the sum arrow linear equivalence product arrow of R and M (from the name)
English
Let $x$, $x_{1}$, $R$ and $M$ be sets. Then the sum arrow linear equivalence product arrow of $R$ and $M$ is a linear equivalence of the set of functions from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to elements of $M$ and $\mathrm{Prod}$ applied to the set of functions from elements of $x$ to elements of $M$ and the set of functions from elements of $x_{1}$ to elements of $M$.
LinearMap.compLeftdefMathlib.LinearAlgebra.Pi, function or constantWording
the left composition of f and I (from the name)
English
Let $f$ be a linear map of $x$ and $x_{1}$. Let $I$ be a set. Then the left composition of $f$ and $I$ is a linear map of the set of functions from elements of $I$ to elements of $x$ and the set of functions from elements of $I$ to elements of $x_{1}$.
LinearMap.constdefMathlib.LinearAlgebra.Pi, function or constantWording
the constant (from the name)
English
The constant is a linear map of $x$ and the set of functions from elements of $x_{1}$ to elements of $x$ defined as the product of the function that maps $x_{5}$ to the identity.
LinearMap.diagdefMathlib.LinearAlgebra.Pi, function or constantWording
the diagonal of i and j (from the name)
English
Let $i$ and $j$ be elements of $x$. Then the diagonal of $i$ and $j$ is a linear map of $x_{2}$ applied to $i$ and $x_{2}$ applied to $j$ defined as $\operatorname{update}$ applied to $0$, $i$, the identity and $j$.
LinearMap.iInfKerProjEquivdefMathlib.LinearAlgebra.Pi, function or constantWording
the infimum kernel projection equivalence of x2 (from the name)
English
Let $R$ be a set. Let $x_{2}$ be a function from elements of $x$ to sets. Assume that $I$ is disjoint to $J$. Assume that $\operatorname{univ} \leq \UnionunionMACRoAB {I}{J}$. Then the infimum kernel projection equivalence of $x_{2}$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{iInf} (\lambda i . \mathrm{iInf} (\lambda h . \operatorname{ker} (\operatorname{proj} (i))))}{x_{6}})}$ and the set of functions from elements $i_{1}$ of $I$ to elements of $x_{2}$ applied to $i_{1}$.
LinearMap.lsumdefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $R$ and $S$ be sets. Let $x_{2}$ be a function from elements of $x$ to sets. Then $\operatorname{lsum}$ applied to $R$, $x_{2}$ and $S$ is a linear equivalence of the set of functions from elements $i$ of $x$ to linear maps of $x_{2}$ applied to $i$ and $M$ and the set of linear maps of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$ and $M$.
LinearMap.pidefMathlib.LinearAlgebra.Pi, function or constantWording
the product of f (from the name)
English
Let $f$ be a function from elements $i_{1}$ of $x_{1}$ to linear maps of $x$ and $x_{5}$ applied to $i_{1}$. Then the product of $i_{1}$ is a linear map of $x$ and the set of functions from elements $i$ of $x_{1}$ to elements of $x_{5}$ applied to $i$.
LinearMap.piMapdefMathlib.LinearAlgebra.Pi, function or constantWording
the product map of f (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ to linear maps of $x_{2}$ applied to $i_{2}$ and $x_{5}$ applied to $i_{2}$. Then the product map of $i_{2}$ is a linear map of the set of functions from elements $i$ of $x$ to elements of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{5}$ applied to $i_{1}$ defined as the function that maps $f$ to the product of the function that maps $i$ to the composition of $i_{2}$ applied to $i$ and the projection of $i$.
LinearMap.projdefMathlib.LinearAlgebra.Pi, function or constantWording
the projection of i (from the name)
English
Let $i$ be an element of $x$. Then the projection of $i$ is a linear map of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$ and $x_{2}$ applied to $i$.
LinearMap.singledefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $R$ be a set. Let $x_{2}$ be a function from elements of $x$ to sets. Let $i$ be an element of $x$. Then $\operatorname{single}$ applied to $R$, $x_{2}$ and $i$ is a linear map of $x_{2}$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $x_{2}$ applied to $i_{1}$.
LinearMap.vecConsdefMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $f$ be a linear map of $M$ and $x$. Let $g$ be a linear map of $M$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x$. Then $\operatorname{vecCons}$ applied to $f$ and $g$ is a linear map of $M$ and the set of functions from elements of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x$ defined as the composition of $\operatorname{toLinearMap}$ applied to $\operatorname{consLinearEquiv}$ applied to $R$ and the function that maps $x_{6}$ to $x$ and the product of $f$ and $g$.
LinearMap.vecCons₂defMathlib.LinearAlgebra.Pi, function or constantEnglish
Let $f$ be a linear map of $M$ and the set of linear maps of $x$ and $x_{1}$. Let $g$ be a linear map of $M$ and the set of linear maps of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $x_{1}$. Then $\mathrm{LinearMap\_\_vecCons\_u2082\_}$ applied to $f$ and $g$ is a linear map of $M$ and the set of linear maps of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to the successor of $n$ to elements of $x_{1}$.
LinearMap.vecEmptydefMathlib.LinearAlgebra.Pi, function or constantEnglish
$\operatorname{vecEmpty}$ is a linear map of $M$ and the set of functions from elements of $\mathrm{Fin}$ applied to $0$ to elements of $x$.
LinearMap.vecEmpty₂defMathlib.LinearAlgebra.Pi, function or constantEnglish
$\mathrm{LinearMap\_\_vecEmpty\_u2082\_}$ is a linear map of $M$ and the set of linear maps of $x$ and the set of functions from elements of $\mathrm{Fin}$ applied to $0$ to elements of $x_{1}$.
Submodule.pidefMathlib.LinearAlgebra.Pi, function or constantWording
the product of I and p (from the name)
English
Let $I$ be an element of $\wp x$. Let $p$ be a function from elements $i_{1}$ of $x$ to submodules of $R$ and $x_{2}$ applied to $i_{1}$. Then the product of $I$ and $i_{1}$ is a submodule of $R$ and the set of functions from elements $i$ of $x$ to elements of $x_{2}$ applied to $i$.
PiTensorProductdefMathlib.LinearAlgebra.PiTensorProduct.Basic, typeWording
product tensor product of R and s (from the name)
English
Let $R$ be a set. Let $s$ be a function from elements of $x$ to sets. Then a product tensor product of $R$ and $s$ is an element of the function that maps $R$ and $s$ to the set of quotients of the additive congruence relation generator of $\operatorname{Eqv}$ applied to $R$ and $s$.
PiTensorProduct.EqvinductiveMathlib.LinearAlgebra.PiTensorProduct.Basic, predicateEnglish
Let $R$ be a set. Let $s$ be a function from elements of $x$ to sets. Let $x_{4}$ be a free additive monoid of $\mathrm{Prod}$ applied to $R$ and the set of functions from elements $i_{1}$ of $x$ to elements of $s$ applied to $i_{1}$. Let $x_{5}$ be a free additive monoid of $\mathrm{Prod}$ applied to $R$ and the set of functions from elements $i$ of $x$ to elements of $s$ applied to $i$. Then we can say that $\operatorname{Eqv}$ holds for $R$, $s$, $x_{4}$ and $x_{5}$.
PiTensorProduct.congrdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the congruence of f (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ to linear equivalences of $s$ applied to $i_{2}$ and $t$ applied to $i_{2}$. Then the congruence of $i_{2}$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $t$ applied to $i_{1}$.
PiTensorProduct.isEmptyEquivdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the tensor product of x (from the docstring)
English
Let $x$ be a set. Then the tensor product of $x$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and $R$.
PiTensorProduct.liftdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the lift (from the name)
English
The lift is a linear equivalence of the set of multilinear maps of $s$ and $E$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and $E$.
PiTensorProduct.liftAddHomdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the lift additive homomorphism of x5 (from the name)
English
Let $x_{5}$ be a function from elements of $\mathrm{Prod}$ applied to $R$ and the set of functions from elements $i_{9}$ of $x$ to elements of $s$ applied to $i_{9}$ to elements of $F$ such that for all elements $r_{3}$ of $R$, for all functions $f_{4}$ from elements $i_{8}$ of $x$ to elements of $s$ applied to $i_{8}$, for all elements $i_{7}$ of $x$, if $\EqtMACRoH {f_{4} (i_{7})}{0}$, then $\EqtMACRoH {x_{5} (\ProdmkMACRoU {r_{3}}{f_{4}})}{0}$, for all functions $f_{3}$ from elements $i_{6}$ of $x$ to elements of $s$ applied to $i_{6}$, $\EqtMACRoH {x_{5} (\ProdmkMACRoU {0}{f_{3}})}{0}$, for all elements $x_{7}$ of $\mathrm{DecidableEq}$ applied to $x$, for all elements $r_{2}$ of $R$, for all functions $f_{2}$ from elements $i_{5}$ of $x$ to elements of $s$ applied to $i_{5}$, for all elements $i_{4}$ of $x$, for all elements $x_{8}$ of $s$ applied to $i_{4}$, for all elements $x_{9}$ of $s$ applied to $i_{4}$, $\EqtMACRoH {x_{5} (\ProdmkMACRoU {r_{2}}{\operatorname{update} (f_{2} , i_{4} , x_{8})})+ x_{5} (\ProdmkMACRoU {r_{2}}{\operatorname{update} (f_{2} , i_{4} , x_{9})})}{x_{5} (\ProdmkMACRoU {r_{2}}{\operatorname{update} (f_{2} , i_{4} , x_{8} + x_{9})})}$, for all elements $r_{1}$ of $R$, for all elements $\mathrm{r'1}$ of $R$, for all functions $f_{1}$ from elements $i_{3}$ of $x$ to elements of $s$ applied to $i_{3}$, $\EqtMACRoH {x_{5} (\ProdmkMACRoU {r_{1}}{f_{1}})+ x_{5} (\ProdmkMACRoU {\mathrm{r'1}}{f_{1}})}{x_{5} (\ProdmkMACRoU {(r_{1} + \mathrm{r'1})}{f_{1}})}$ and for all elements $x_{6}$ of $\mathrm{DecidableEq}$ applied to $x$, for all elements $r$ of $R$, for all functions $f$ from elements $i_{2}$ of $x$ to elements of $s$ applied to $i_{2}$, for all elements $i_{1}$ of $x$, for all elements $\mathrm{r'}$ of $R$, $\EqtMACRoH {x_{5} (\ProdmkMACRoU {r}{\operatorname{update} (f , i_{1} , \HSMulhSMulMACRoAL {\mathrm{r'}}{f (i_{1})})})}{x_{5} (\ProdmkMACRoU {(\mathrm{r'} \times r)}{f})}$. Then the lift additive homomorphism of $x_{5}$ is an additive monoid homomorphism of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and $F$.
PiTensorProduct.liftsdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the lift of x4 (from the name)
English
Let $x_{4}$ be a product tensor product of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$. Then the lift of $x_{4}$ is an element of the power set of the set of free additive monoids of $\mathrm{Prod}$ applied to $R$ and the set of functions from elements $i$ of $x$ to elements of $s$ applied to $i$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that the morphism into the quotient by an additive congruence relation of $p$ is equal to $x_{4}$.
PiTensorProduct.mapdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the map of f (from the name)
English
Let $f$ be a function from elements $i_{2}$ of $x$ to linear maps of $s$ applied to $i_{2}$ and $t$ applied to $i_{2}$. Then the map of $i_{2}$ is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $t$ applied to $i_{1}$ defined as the function that maps $f$ to $\operatorname{lift}$ applied to the composition linear map of $\operatorname{tprod}$ applied to $R$ and $i_{2}$ and $f$.
PiTensorProduct.mapIncldefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the map inclusion of p (from the name)
English
Let $p$ be a function from elements $i_{2}$ of $x$ to submodules of $R$ and $s$ applied to $i_{2}$. Then the map inclusion of $i_{2}$ is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p (i)}{x_{4}})}$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$ defined as the function that maps $p$ to the map of the function that maps $i$ to the subtype of $i_{2}$ applied to $i$.
PiTensorProduct.mapMonoidHomdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the map monoid homomorphism (from the name)
English
The map monoid homomorphism is a monoid homomorphism of the set of functions from elements $i$ of $x$ to linear maps of $s$ applied to $i$ and $s$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $s$ applied to $i_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{map}$ and $\mathrm{PiTensorProduct\_\_map\_one}$ and $\mathrm{PiTensorProduct\_\_map\_mul}$.
PiTensorProduct.mapMultilineardefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantEnglish
Let $R$ be a set. Let $s$ and $t$ be functions from elements of $x$ to sets. Then $\operatorname{mapMultilinear}$ applied to $R$, $s$ and $t$ is a multilinear map of the function that maps $i$ to the set of linear maps of $s$ applied to $i$ and $t$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $t$ applied to $i_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{map}$, the function that maps $x_{6}$, $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ to $\mathrm{PiTensorProduct\_\_map\_update\_add}$ applied to $x_{7}$, $x_{8}$, $x_{9}$ and $x_{10}$ and the function that maps $x_{11}$, $x_{12}$, $x_{13}$, $x_{14}$ and $x_{15}$ to $\mathrm{PiTensorProduct\_\_map\_update\_smul}$ applied to $x_{12}$, $x_{13}$, $x_{14}$ and $x_{15}$.
PiTensorProduct.map₂defMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the map of f (from the name)
English
Let $f$ be a function from elements $i_{3}$ of $x$ to linear maps of $s$ applied to $i_{3}$ and the set of linear maps of $t$ applied to $i_{3}$ and $\mathrm{t'}$ applied to $i_{3}$. Then the map of $i_{3}$ is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $t$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $\mathrm{t'}$ applied to $i_{2}$ defined as the function that maps $f$ to $\operatorname{lift}$ applied to the composition multilinear map of the product tensor homomorphism map and the composition linear map of $\operatorname{tprod}$ applied to $R$ and $i_{3}$ and $f$.
PiTensorProduct.piTensorHomMapdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the product tensor homomorphism map (from the name)
English
The product tensor homomorphism map is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to the set of linear maps of $s$ applied to $i$ and $t$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $t$ applied to $i_{2}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the lift and $\operatorname{lift}$ applied to $\operatorname{piLinearMap}$ applied to $\operatorname{tprod}$ applied to $R$.
PiTensorProduct.piTensorHomMapFun₂defMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the product tensor homomorphism map function of x8 (from the name)
English
Let $x_{8}$ be a product tensor product of $R$ and the function that maps $i_{3}$ to the set of linear maps of $s$ applied to $i_{3}$ and the set of linear maps of $t$ applied to $i_{3}$ and $\mathrm{t'}$ applied to $i_{3}$. Then the product tensor homomorphism map function of $x_{8}$ is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $t$ applied to $i_{1}$ and the set of product tensor products of $R$ and the function that maps $i_{2}$ to $\mathrm{t'}$ applied to $i_{2}$ defined as $\operatorname{lift}$ applied to the composition multilinear map of the product tensor homomorphism map and $\operatorname{coe}$ applied to the lift, $\operatorname{piLinearMap}$ applied to $\operatorname{tprod}$ applied to $R$ and $x_{8}$.
PiTensorProduct.piTensorHomMap₂defMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the product tensor homomorphism map (from the name)
English
The product tensor homomorphism map is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to the set of linear maps of $s$ applied to $i$ and the set of linear maps of $t$ applied to $i$ and $\mathrm{t'}$ applied to $i$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $i_{1}$ and the set of linear maps of the set of product tensor products of $R$ and the function that maps $i_{2}$ to $t$ applied to $i_{2}$ and the set of product tensor products of $R$ and the function that maps $i_{3}$ to $\mathrm{t'}$ applied to $i_{3}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{PiTensorProduct\_\_piTensorHomMapFun\_u2082\_}$ and the function that maps $x_{8}$ and $y$ to $\mathrm{PiTensorProduct\_\_piTensorHomMapFun\_u2082\_\_add}$ applied to $x_{8}$ and $y$ and the function that maps $x_{9}$ and $y_{1}$ to $\mathrm{PiTensorProduct\_\_piTensorHomMapFun\_u2082\_\_smul}$ applied to $x_{9}$ and $y_{1}$.
PiTensorProduct.reindexdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the reindexing of s and e (from the name)
English
Let $R$ be a set. Let $s$ be a function from elements of $x$ to sets. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $s$ and $e$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $s$ applied to $\operatorname{symm}$ applied to $e$ and $i_{1}$.
PiTensorProduct.subsingletonEquivdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantWording
the subsingleton equivalence of x4 (from the name)
English
Let $x_{4}$ be an element of $x$. Then the subsingleton equivalence of $x_{4}$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$ and $s$ applied to $x_{4}$.
PiTensorProduct.tmulEquivdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{tmulEquiv}$ applied to $R$ and $M$ is a linear equivalence of the set of tensor products of the set of product tensor products of $R$ and the function that maps $x_{5}$ to $M$ and the set of product tensor products of $R$ and the function that maps $x_{6}$ to $M$ and the set of product tensor products of $R$ and the function that maps $x_{7}$ to $M$ defined as $\operatorname{tmulEquivDep}$ applied to $R$ and the function that maps $x_{5}$ to $M$.
PiTensorProduct.tmulEquivDepdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantEnglish
Let $R$ be a set. Let $N$ be a function from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to sets. Then $\operatorname{tmulEquivDep}$ applied to $R$ and $N$ is a linear equivalence of the set of tensor products of the set of product tensor products of $R$ and the function that maps $x_{5}$ to $N$ applied to $\operatorname{inl}$ applied to $x_{5}$ and the set of product tensor products of $R$ and the function that maps $x_{6}$ to $N$ applied to $\operatorname{inr}$ applied to $x_{6}$ and the set of product tensor products of $R$ and the function that maps $i$ to $N$ applied to $i$.
PiTensorProduct.tproddefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantEnglish
Let $R$ be a set. Then $\operatorname{tprod}$ applied to $R$ is a multilinear map of $s$ and the set of product tensor products of $R$ and the function that maps $i$ to $s$ applied to $i$.
PiTensorProduct.tprodCoeffdefMathlib.LinearAlgebra.PiTensorProduct.Basic, function or constantEnglish
Let $R$ be a set. Let $r$ be an element of $R$. Let $f$ be a function from elements $i_{1}$ of $x$ to elements of $s$ applied to $i_{1}$. Then $\operatorname{tprodCoeff}$ applied to $R$, $r$, $i_{1}$ and $f$ is a product tensor product of $R$ and the function that maps $i$ to $s$ applied to $i$ defined as the function that maps $f$ to $\operatorname{mk'}$ applied to the additive congruence relation generator of $\operatorname{Eqv}$ applied to $R$ and the function that maps $i_{5}$ to $s$ applied to $i_{5}$, $\operatorname{of}$ applied to $\ProdmkMACRoU {r}{i_{1}}$ and $f$.
Basis.piTensorProductdefMathlib.LinearAlgebra.PiTensorProduct.Basis, function or constantWording
the product tensor product of b (from the name)
English
Let $b$ be a function from elements $i_{2}$ of $x$ to bases of $R$ and $M$ applied to $i_{2}$. Then the product tensor product of $i_{2}$ is a basis of $R$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the function that maps $b$ to the map of the basis single one and the inverse of the composition of the composition of the congruence of the function that maps $i$ to the representation of $i_{2}$ applied to $i$ and the product tensor product and $\operatorname{lcongr}$ applied to the identity of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ and the linear equivalence of the constant base ring isomorphism of $x$ and $R$.
PiTensorProduct.ofDFinsuppEquivdefMathlib.LinearAlgebra.PiTensorProduct.DFinsupp, function or constantWording
the product tensor product (from the name)
English
The product tensor product is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to the set of finitely supported functions of the function that maps $j$ to $M$ applied to $i$ and $j$ and the set of finitely supported functions of the function that maps $p$ to the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $p$ applied to $i_{1}$.
PiTensorProduct.ofDirectSumEquivdefMathlib.LinearAlgebra.PiTensorProduct.DirectSum, function or constantWording
the product tensor product (from the name)
English
The product tensor product is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to the set of direct sums of $x_{1}$ applied to $i$ and the function that maps $j$ to $M$ applied to $i$ and $j$ and the set of direct sums of the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ and the function that maps $p$ to the set of product tensor products of $R$ and the function that maps $i_{2}$ to $M$ applied to $i_{2}$ and $p$ applied to $i_{2}$ defined as the product tensor product.
PiTensorProduct.dualDistribdefMathlib.LinearAlgebra.PiTensorProduct.Dual, function or constantEnglish
$\operatorname{dualDistrib}$ is a linear map of the set of product tensor products of $R$ and the function that maps $i$ to the set of duals of $R$ and $M$ applied to $i$ and the set of duals of $R$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the composition of the right composition of $R$ and the linear map of the constant base ring isomorphism of $x$ and $R$ and the product tensor homomorphism map.
PiTensorProduct.dualDistribEquivdefMathlib.LinearAlgebra.PiTensorProduct.Dual, function or constantWording
the dual distributive equivalence (from the name)
English
The dual distributive equivalence is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to the set of duals of $R$ and $M$ applied to $i$ and the set of duals of $R$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the dual distributive equivalence of the function that maps $i$ to $\operatorname{chooseBasis}$ applied to $R$ and $M$ applied to $i$.
PiTensorProduct.dualDistribEquivOfBasisdefMathlib.LinearAlgebra.PiTensorProduct.Dual, function or constantWording
the dual distributive equivalence of b (from the name)
English
Let $b$ be a function from elements $i_{2}$ of $x$ to bases of $R$ and $M$ applied to $i_{2}$. Then the dual distributive equivalence of $i_{2}$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to the set of duals of $R$ and $M$ applied to $i$ and the set of duals of $R$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the function that maps $b$ to the linear equivalence of $\operatorname{dualDistrib}$ and the dual distributive inverse of $i_{2}$.
PiTensorProduct.dualDistribInvOfBasisdefMathlib.LinearAlgebra.PiTensorProduct.Dual, function or constantWording
the dual distributive inverse of b (from the name)
English
Let $b$ be a function from elements $i_{2}$ of $x$ to bases of $R$ and $M$ applied to $i_{2}$. Then the dual distributive inverse of $i_{2}$ is a linear map of the set of duals of $R$ and the set of product tensor products of $R$ and the function that maps $i$ to $M$ applied to $i$ and the set of product tensor products of $R$ and the function that maps $i_{1}$ to the set of duals of $R$ and $M$ applied to $i_{1}$ defined as the function that maps $b$ to $\FinsetSum {\FinsetunivMACRoAC}{p}{\operatorname{comp} (\operatorname{symm} (\operatorname{ringLmapEquivSelf} (R , \Natural , \mathrm{PiTensorProduct} (R , \lambda i_{4} . \operatorname{Dual} (R , M (i_{4})))), \operatorname{tprod} (R , \lambda i_{7} . \operatorname{dualBasis} (i_{2} (i_{7}), p (i_{7})))), \mathrm{LinearMap\_\_apply\_u2097\_\_\_app} (\operatorname{tprod} (R , \lambda i_{10} . i_{2} (i_{10} , p (i_{10})))))}{b}$.
PiTensorProduct.ofFinsuppEquivdefMathlib.LinearAlgebra.PiTensorProduct.Finsupp, function or constantWording
the product tensor product (from the name)
English
The product tensor product is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $\FinsuppMACRoQ {x_{1} (i)}{M (i)}$ and the set of finitely supported functions from the set of functions from elements $i_{1}$ of $x$ to elements of $x_{1}$ applied to $i_{1}$ to the set of product tensor products of $R$ and the function that maps $i_{2}$ to $M$ applied to $i_{2}$ defined as the composition of the composition of the congruence of the function that maps $x_{9}$ to the finitely supported function linear equivalence finitely supported function of $R$ and the product tensor product and the inverse of the finitely supported function linear equivalence finitely supported function of $R$.
PiTensorProduct.ofFinsuppEquiv'defMathlib.LinearAlgebra.PiTensorProduct.Finsupp, function or constantWording
the product tensor product (from the name)
English
The product tensor product is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $\FinsuppMACRoQ {x_{1} (i)}{R}$ and $\FinsuppMACRoQ {(\mathrm{Elem} (x)\rightarrow x_{1} (i_{1}))}{R}$ defined as the composition of the product tensor product and $\operatorname{lcongr}$ applied to the identity of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and the linear equivalence of the constant base ring isomorphism of $x$ and $R$.
PiTensorProduct.equivPiTensorComplSingletonTensordefMathlib.LinearAlgebra.PiTensorProduct.Generators, function or constantWording
the equivalence product tensor complement singleton tensor of M and x5 (from the name)
English
Let $R$ be a set. Let $M$ be a function from elements of $x$ to sets. Let $x_{5}$ be an element of $x$. Then the equivalence product tensor complement singleton tensor of $M$ and $x_{5}$ is a linear equivalence of the set of product tensor products of $R$ and the function that maps $i$ to $M$ applied to $i$ and the set of tensor products of the set of product tensor products of $R$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $M$ applied to $x_{5}$ defined as the composition of the reindexing of $M$ and the inverse of $\operatorname{subtypeNeSumPUnit}$ applied to $x_{5}$ and the composition of the inverse of $\operatorname{tmulEquivDep}$ applied to $R$ and the function that maps $i$ to $M$ applied to $\operatorname{subtypeNeSumPUnit}$ applied to $x_{5}$ and $i$ and the tensor of the set of product tensor products of $R$ and the function that maps $x_{6}$ to $M$ applied to $\operatorname{subtypeNeSumPUnit}$ applied to $x_{5}$ and $\operatorname{inl}$ applied to $x_{6}$ and the subsingleton equivalence of $\operatorname{unit}$.
LinearEquiv.prodAssocdefMathlib.LinearAlgebra.Prod, function or constantWording
the product associator of x1 and x2 (from the name)
English
Let $R$, $x$, $x_{1}$ and $x_{2}$ be sets. Then the product associator of $x_{1}$ and $x_{2}$ is a linear equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
LinearEquiv.prodCommdefMathlib.LinearAlgebra.Prod, function or constantEnglish
Let $R$, $M$ and $N$ be sets. Then $\operatorname{prodComm}$ applied to $R$, $M$ and $N$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $N$ and $M$.
LinearEquiv.prodCongrdefMathlib.LinearAlgebra.Prod, function or constantWording
the product congruence of x11 and x12 (from the name)
English
Let $x_{11}$ be a linear equivalence of $M$ and $x$. Let $x_{12}$ be a linear equivalence of $x_{1}$ and $x_{2}$. Then the product congruence of $x_{11}$ and $x_{12}$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{2}$.
LinearEquiv.prodProdProdCommdefMathlib.LinearAlgebra.Prod, function or constantEnglish
Let $R$, $M$, $x$, $x_{1}$ and $x_{2}$ be sets. Then $\operatorname{prodProdProdComm}$ applied to $R$, $M$, $x$, $x_{1}$ and $x_{2}$ is a linear equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $M$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{2}$.
LinearEquiv.prodUniquedefMathlib.LinearAlgebra.Prod, function or constantEnglish
$\operatorname{prodUnique}$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ and $x$ and $M$.
LinearEquiv.skewProddefMathlib.LinearAlgebra.Prod, function or constantWording
the skew product of x12 and f (from the name)
English
Let $x_{11}$ be a linear equivalence of $M$ and $x$. Let $x_{12}$ be a linear equivalence of $x_{1}$ and $x_{2}$. Let $f$ be a linear map of $M$ and $x_{2}$. Then the skew product of $x_{12}$ and $f$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{2}$.
LinearEquiv.skewSwapdefMathlib.LinearAlgebra.Prod, function or constantWording
the skew swap of M and N (from the name)
English
Let $R$, $M$ and $N$ be sets. Then the skew swap of $M$ and $N$ is a linear equivalence of $\mathrm{Prod}$ applied to $M$ and $N$ and $\mathrm{Prod}$ applied to $N$ and $M$.
LinearEquiv.uniqueProddefMathlib.LinearAlgebra.Prod, function or constantWording
the unique product (from the name)
English
The unique product is a linear equivalence of $\mathrm{Prod}$ applied to $x$ and $M$ and $M$.
LinearMap.coproddefMathlib.LinearAlgebra.Prod, function or constantWording
the coprod function of f and g (from the docstring)
English
Let $f$ be a linear map of $M$ and $x_{1}$. Let $g$ be a linear map of $x$ and $x_{1}$. Then the coprod function of $f$ and $g$ is a linear map of $\mathrm{Prod}$ applied to $M$ and $x$ and $x_{1}$ defined as the sum of the composition of $f$ and the first component of $M$ and $x$ and the composition of $g$ and the second component of $M$ and $x$.
LinearMap.coprodEquivdefMathlib.LinearAlgebra.Prod, function or constantWording
the coproduct equivalence of S (from the name)
English
Let $S$ be a set. Then the coproduct equivalence of $S$ is a linear equivalence of $\mathrm{Prod}$ applied to the set of linear maps of $M$ and $x_{1}$ and the set of linear maps of $x$ and $x_{1}$ and the set of linear maps of $\mathrm{Prod}$ applied to $M$ and $x$ and $x_{1}$.
LinearMap.fstdefMathlib.LinearAlgebra.Prod, function or constantWording
the first component of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the first component of $M$ and $x$ is a linear map of $\mathrm{Prod}$ applied to $M$ and $x$ and $M$.
LinearMap.graphdefMathlib.LinearAlgebra.Prod, function or constantWording
the graph of f (from the name)
English
Let $f$ be a linear map of $M$ and $x$. Then the graph of $f$ is a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $x$.
LinearMap.inldefMathlib.LinearAlgebra.Prod, function or constantWording
the left injection of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the left injection of $M$ and $x$ is a linear map of $M$ and $\mathrm{Prod}$ applied to $M$ and $x$ defined as the product of the identity and $0$.
LinearMap.inrdefMathlib.LinearAlgebra.Prod, function or constantWording
the right injection of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the right injection of $M$ and $x$ is a linear map of $x$ and $\mathrm{Prod}$ applied to $M$ and $x$ defined as the product of $0$ and the identity.
LinearMap.kerComplementEquivRangedefMathlib.LinearAlgebra.Prod, function or constantWording
the kernel complement equivalence range of f and h (from the name)
English
Let $f$ be a linear map of $M$ and $x$ such that $\mathrm{IsCompl}$ holds for $C$ and the kernel of $f$. Then the kernel complement equivalence range of $f$ and $h$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {C}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{7}})}$.
LinearMap.proddefMathlib.LinearAlgebra.Prod, function or constantWording
the product of f and g (from the name)
English
Let $f$ be a linear map of $M$ and $x$. Let $g$ be a linear map of $M$ and $x_{1}$. Then the product of $f$ and $g$ is a linear map of $M$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
LinearMap.prodEquivdefMathlib.LinearAlgebra.Prod, function or constantWording
the product equivalence of S (from the name)
English
Let $S$ be a set. Then the product equivalence of $S$ is a linear equivalence of $\mathrm{Prod}$ applied to the set of linear maps of $M$ and $x$ and the set of linear maps of $M$ and $x_{1}$ and the set of linear maps of $M$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.
LinearMap.prodMapdefMathlib.LinearAlgebra.Prod, function or constantWording
the product map of f and g (from the name)
English
Let $f$ be a linear map of $M$ and $x_{1}$. Let $g$ be a linear map of $x$ and $x_{2}$. Then the product map of $f$ and $g$ is a linear map of $\mathrm{Prod}$ applied to $M$ and $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ defined as the product of the composition of $f$ and the first component of $M$ and $x$ and the composition of $g$ and the second component of $M$ and $x$.
LinearMap.prodMapAlgHomdefMathlib.LinearAlgebra.Prod, function or constantWording
the product map algebra homomorphism of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the product map algebra homomorphism of $M$ and $x$ is an algebra homomorphism of $\mathrm{Prod}$ applied to the set of ends of $R$ and $M$ and the set of ends of $R$ and $x$ and the set of ends of $R$ and $\mathrm{Prod}$ applied to $M$ and $x$.
LinearMap.prodMapLineardefMathlib.LinearAlgebra.Prod, function or constantEnglish
Let $R$, $M$, $x$, $x_{1}$, $x_{2}$ and $S$ be sets. Then $\operatorname{prodMapLinear}$ applied to $R$, $M$, $x$, $x_{1}$, $x_{2}$ and $S$ is a linear map of $\mathrm{Prod}$ applied to the set of linear maps of $M$ and $x_{1}$ and the set of linear maps of $x$ and $x_{2}$ and the set of linear maps of $\mathrm{Prod}$ applied to $M$ and $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.
LinearMap.prodMapRingHomdefMathlib.LinearAlgebra.Prod, function or constantWording
the product map ring homomorphism of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the product map ring homomorphism of $M$ and $x$ is a ring homomorphism of $\mathrm{Prod}$ applied to the set of linear maps of $M$ and $M$ and the set of linear maps of $x$ and $x$ and the set of linear maps of $\mathrm{Prod}$ applied to $M$ and $x$ and $\mathrm{Prod}$ applied to $M$ and $x$.
LinearMap.snddefMathlib.LinearAlgebra.Prod, function or constantWording
the second component of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the second component of $M$ and $x$ is a linear map of $\mathrm{Prod}$ applied to $M$ and $x$ and $x$.
Submodule.fstdefMathlib.LinearAlgebra.Prod, function or constantWording
the first component of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the first component of $M$ and $x$ is a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $x$ defined as the preimage of the second component of $M$ and $x$ and the bottom.
Submodule.fstEquivdefMathlib.LinearAlgebra.Prod, function or constantWording
the first component equivalence of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the first component equivalence of $M$ and $x$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{fst} (M , x)}{x_{6}})}$ and $M$.
Submodule.snddefMathlib.LinearAlgebra.Prod, function or constantWording
the second component of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the second component of $M$ and $x$ is a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $x$ defined as the preimage of the first component of $M$ and $x$ and the bottom.
Submodule.sndEquivdefMathlib.LinearAlgebra.Prod, function or constantWording
the second component equivalence of M and x (from the name)
English
Let $R$, $M$ and $x$ be sets. Then the second component equivalence of $M$ and $x$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{snd} (M , x)}{x_{6}})}$ and $x$.
LinearMap.IsProjstructureMathlib.LinearAlgebra.Projection, predicateEnglish
Let $m$ be a submodule of $S$ and $M$. Let $f$ be an element of $F$. Then we can say that $\operatorname{IsProj}$ holds for $m$ and $f$.
LinearMap.IsProj.codRestrictdefMathlib.LinearAlgebra.Projection, function or constantEnglish
Assume that $\operatorname{IsProj}$ holds for $m$ and $f$. Then $\operatorname{codRestrict}$ applied to $h$ is a linear map of $M$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {m}{x_{3}})}$.
LinearMap.equivProdOfSurjectiveOfIsCompldefMathlib.LinearAlgebra.Projection, function or constantWording
the equivalence product of f and g (from the name)
English
Let $f$ be a linear map of $E$ and $F$. Let $g$ be a linear map of $E$ and $G$. Assume that the range of $f$ is equal to the top. Assume that the range of $g$ is equal to the top. Assume that $\mathrm{IsCompl}$ holds for the kernel of $f$ and the kernel of $g$. Then the equivalence product of $f$ and $g$ is a linear equivalence of $E$ and $\mathrm{Prod}$ applied to $F$ and $G$.
LinearMap.linearProjOfIsCompldefMathlib.LinearAlgebra.Projection, function or constantWording
the linear projection of q and i (from the name)
English
Let $q$ be a submodule of $R$ and $E$. Let $i$ be a linear map of $F$ and $E$ such that $\operatorname{coe}$ applied to $i$ is injective and $\mathrm{IsCompl}$ holds for the range of $i$ and $q$. Then the linear projection of $q$ and $i$ is a linear map of $E$ and $F$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $i$ and $\mathrm{hi}$ and $\operatorname{projectionOnto}$ applied to the range of $i$, $q$ and $h$.
LinearMap.ofIsCompldefMathlib.LinearAlgebra.Projection, function or constantWording
the linear map of x5 and x6 (from the name)
English
Assume that $\mathrm{IsCompl}$ holds for $p$ and $q$. Let $x_{5}$ be a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {p}{x_{8}})}$ and $F$. Let $x_{6}$ be a linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {q}{x_{7}})}$ and $F$. Then the linear map of $x_{5}$ and $x_{6}$ is a linear map of $E$ and $F$ defined as the composition of the coprod function of $x_{5}$ and $x_{6}$ and $\operatorname{toLinearMap}$ applied to the inverse of the product equivalence of $p$ and $q$.
LinearMap.ofIsComplProddefMathlib.LinearAlgebra.Projection, function or constantWording
the linear map of h (from the name)
English
Assume that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then the linear map of $h$ is a linear map of $\mathrm{Prod}$ applied to the set of linear maps of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $F$ and the set of linear maps of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {q}{x_{7}})}$ and $F$ and the set of linear maps of $E$ and $F$.
LinearMap.ofIsComplProdEquivdefMathlib.LinearAlgebra.Projection, function or constantWording
the linear map of h (from the name)
English
Assume that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then the linear map of $h$ is a linear equivalence of $\mathrm{Prod}$ applied to the set of linear maps of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $F$ and the set of linear maps of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {q}{x_{7}})}$ and $F$ and the set of linear maps of $E$ and $F$.
Submodule.isComplEquivProjdefMathlib.LinearAlgebra.Projection, function or constantEnglish
Let $p$ be a submodule of $R$ and $E$. Then $\operatorname{isComplEquivProj}$ applied to $p$ is an equivalence from $\SubtypeSet {q}{\mathrm{IsCompl} (p , q)}$ to $\SubtypeSet {f}{\mathrm{forall} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}, \lambda x_{3} . \EqtMACRoH {f (x_{3})}{x_{3}})}$.
Submodule.isIdempotentElemEquivdefMathlib.LinearAlgebra.Projection, function or constantEnglish
Let $p$ be a submodule of $R$ and $E$. Then $\operatorname{isIdempotentElemEquiv}$ applied to $p$ is an element of $\EquivMACRoAE {(\SubtypeSet {f}{\mathrm{and} (\mathrm{IsIdempotentElem} (f), \EqtMACRoH {\operatorname{range} (f)}{p})})}{(\SubtypeSet {f_{1}}{\mathrm{forall} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}, \lambda x_{3} . \EqtMACRoH {f_{1} (x_{3})}{x_{3}})})}$.
Submodule.prodEquivOfIsCompldefMathlib.LinearAlgebra.Projection, function or constantWording
the product equivalence of p and q (from the name)
English
Let $p$ and $q$ be submodules of $R$ and $E$ such that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then the product equivalence of $p$ and $q$ is a linear equivalence of $\mathrm{Prod}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {q}{x_{4}})}$ and $E$.
Submodule.projectiondefMathlib.LinearAlgebra.Projection, function or constantWording
the projection of p and q (from the name)
English
Let $p$ and $q$ be submodules of $R$ and $E$ such that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then the projection of $p$ and $q$ is a linear map of $E$ and $E$ defined as the composition of the subtype of $p$ and $\operatorname{projectionOnto}$ applied to $p$, $q$ and $\mathrm{hpq}$.
Submodule.projectionOntodefMathlib.LinearAlgebra.Projection, function or constantEnglish
Let $p$ and $q$ be submodules of $R$ and $E$ such that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then $\operatorname{projectionOnto}$ applied to $p$, $q$ and $h$ is a linear map of $E$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ defined as the composition of the first component of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {q}{x_{4}})}$ and $\operatorname{toLinearMap}$ applied to the inverse of the product equivalence of $p$ and $q$.
Submodule.quotientEquivOfIsCompldefMathlib.LinearAlgebra.Projection, function or constantWording
the quotient equivalence of p and q (from the name)
English
Let $p$ and $q$ be submodules of $R$ and $E$ such that $\mathrm{IsCompl}$ holds for $p$ and $q$. Then the quotient equivalence of $p$ and $q$ is a linear equivalence of the set of quotients of $E$ and $p$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {q}{x_{3}})}$.
Projectivization.PSLAction.toPermHomdefMathlib.LinearAlgebra.Projectivization.Action, function or constantWording
the permutation homomorphism (from the name)
English
The permutation homomorphism is a monoid homomorphism of the set of projective special linear groups of $x_{1}$ and $K$ and the set of permutations of the set of projectivizations of $K$ and the set of functions from elements of $x_{1}$ to elements of $K$.
ProjectivizationdefMathlib.LinearAlgebra.Projectivization.Basic, typeWording
projectivization of K and V (from the name)
English
Let $K$ and $V$ be sets. Then a projectivization of $K$ and $V$ is an element of the function that maps $K$ and $V$ to $\mathrm{Quotient}$ applied to $\mathrm{projectivizationSetoid}$ applied to $K$ and $V$.
Projectivization.equivSubmoduledefMathlib.LinearAlgebra.Projectivization.Basic, function or constantWording
the equivalence submodule of K and V (from the name)
English
Let $K$ and $V$ be sets. Then the equivalence submodule of $K$ and $V$ is an element of $\EquivMACRoAE {\mathrm{Projectivization} (K , V)}{(\SubtypeSet {H}{\mathrm{Eq} (\operatorname{finrank} (K , \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}), 1)})}$.
Projectivization.liftdefMathlib.LinearAlgebra.Projectivization.Basic, function or constantWording
the lift of f and x4 (from the name)
English
Let $f$ be a function from elements of $\SubtypeSet {v_{2}}{\mathrm{Neq} (v_{2} , 0)}$ to elements of $x_{3}$ such that for all elements $a$ of $\SubtypeSet {v_{1}}{\mathrm{Neq} (v_{1} , 0)}$, for all elements $b$ of $\SubtypeSet {v}{\mathrm{Neq} (v , 0)}$, for all elements $t$ of $K$, if $\EqtMACRoH {a}{\HSMulhSMulMACRoAL {t}{b}}$, then $\EqtMACRoH {f (a)}{f (b)}$. Let $x_{4}$ be a projectivization of $K$ and $V$. Then the lift of $f$ and $x_{4}$ is an element of $x_{3}$.
Projectivization.mapdefMathlib.LinearAlgebra.Projectivization.Basic, function or constantWording
the map of f and x7 (from the name)
English
Let $f$ be a linear map of $V$ and $W$ such that $\operatorname{coe}$ applied to $f$ is injective. Let $x_{7}$ be a projectivization of $K$ and $V$. Then the map of $f$ and $x_{7}$ is a projectivization of $L$ and $W$.
Projectivization.mkdefMathlib.LinearAlgebra.Projectivization.Basic, function or constantEnglish
Let $K$ be a set. Let $v$ be an element of $V$ such that $v \neq 0$. Then $\operatorname{mk}$ applied to $K$, $v$ and $\mathrm{hv}$ is a projectivization of $K$ and $V$ defined as $\operatorname{mk''}$ applied to $v$.
Projectivization.mk'defMathlib.LinearAlgebra.Projectivization.Basic, function or constantEnglish
Let $K$ be a set. Let $v$ be an element of $\SubtypeSet {v_{1}}{\mathrm{Neq} (v_{1} , 0)}$. Then $\operatorname{mk'}$ applied to $K$ and $v$ is a projectivization of $K$ and $V$ defined as $\operatorname{mk''}$ applied to $v$.
Projectivization.mk''defMathlib.LinearAlgebra.Projectivization.Basic, function or constantEnglish
Let $H$ be a submodule of $K$ and $V$ such that the rank of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ is equal to $1$. Then $\operatorname{mk''}$ applied to $H$ and $h$ is a projectivization of $K$ and $V$ defined as $\operatorname{symm}$ applied to the equivalence submodule of $K$ and $V$ and $H$.
Projectivization.repdefMathlib.LinearAlgebra.Projectivization.Basic, function or constantWording
the representation of v (from the name)
English
Let $v$ be a projectivization of $K$ and $V$. Then the representation of $v$ is an element of $V$ defined as $\operatorname{out}$ applied to $v$.
Projectivization.submoduledefMathlib.LinearAlgebra.Projectivization.Basic, function or constantWording
the submodule of v (from the name)
English
Let $v$ be a projectivization of $K$ and $V$. Then the submodule of $v$ is a submodule of $K$ and $V$.
Projectivization.equivQuotientOrbitReldefMathlib.LinearAlgebra.Projectivization.Cardinality, function or constantWording
the equivalence quotient orbit relation of k and V (from the name)
English
Let $k$ and $V$ be sets. Then the equivalence quotient orbit relation of $k$ and $V$ is an equivalence from the set of projectivizations of $k$ and $V$ to $\mathrm{Quotient}$ applied to $\operatorname{orbitRel}$ applied to $\UnitsMACRoAO {k}$ and $\SubtypeSet {v}{\mathrm{Neq} (v , 0)}$.
Projectivization.nonZeroEquivProjectivizationProdUnitsdefMathlib.LinearAlgebra.Projectivization.Cardinality, function or constantWording
the non zero equivalence projectivization product unit of k and V (from the name)
English
Let $k$ and $V$ be sets. Then the non zero equivalence projectivization product unit of $k$ and $V$ is an equivalence from $\SubtypeSet {v}{\mathrm{Neq} (v , 0)}$ to $\mathrm{Prod}$ applied to the set of projectivizations of $k$ and $V$ and $\UnitsMACRoAO {k}$.
Projectivization.IsCollineardefMathlib.LinearAlgebra.Projectivization.Collinear, predicateWording
S is collinear (from the name)
English
Let $S$ be an element of the power set of the set of projectivizations of $K$ and $V$. Then $S$ is collinear, if there exists a subspace $M$ of $K$ and $V$, such that $\operatorname{Finite}$ holds for $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{submodule} (M)}{x_{3}})}$, the rank of $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{submodule} (M)}{x_{4}})}$ is less than or equal to $2$ and $S \leq M$.
Projectivization.crossdefMathlib.LinearAlgebra.Projectivization.Constructions, function or constantEnglish
Let $x_{2}$ and $x_{3}$ be projectivizations of $F$ and the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$. Then $\operatorname{cross}$ applied to $x_{2}$ and $x_{3}$ is a projectivization of $F$ and the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $F$.
Projectivization.orthogonaldefMathlib.LinearAlgebra.Projectivization.Constructions, predicateWording
x2 is orthogonal to x3 (from the name)
English
Let $x_{2}$ and $x_{3}$ be projectivizations of $F$ and the set of functions from elements of $m$ to elements of $F$. Then we can say that $x_{2}$ is orthogonal to $x_{3}$.
Projectivization.DependentinductiveMathlib.LinearAlgebra.Projectivization.Independence, predicateWording
x4 is dependent (from the name)
English
Let $x_{4}$ be a function from elements of $x$ to projectivizations of $K$ and $V$. Then we can say that $x_{4}$ is dependent.
Projectivization.IndependentinductiveMathlib.LinearAlgebra.Projectivization.Independence, predicateWording
x4 is independent (from the name)
English
Let $x_{4}$ be a function from elements of $x$ to projectivizations of $K$ and $V$. Then we can say that $x_{4}$ is independent.
PSL2.IwasawadefMathlib.LinearAlgebra.Projectivization.PSL.PSL2, function or constantEnglish
$\operatorname{Iwasawa}$ is an element of $\operatorname{IwasawaStructure}$ applied to the set of projective special linear groups of $\mathrm{Fin}$ applied to $2$ and $F$ and the set of projectivizations of $F$ and the set of functions from elements of $\mathrm{Fin}$ applied to $2$ to elements of $F$.
Matrix.SpecialLinearGroup.lineStabdefMathlib.LinearAlgebra.Projectivization.PSL.Stabilizer, function or constantEnglish
Let $L$ be a submodule of $F$ and the set of functions from elements of $x_{1}$ to elements of $F$. Then $\operatorname{lineStab}$ applied to $L$ is a subgroup of the set of special linear groups of $x_{1}$ and $F$.
PSL.iwasawaTdefMathlib.LinearAlgebra.Projectivization.PSL.Stabilizer, function or constantEnglish
Let $p$ be a projectivization of $F$ and the set of functions from elements of $x_{1}$ to elements of $F$. Then $\operatorname{iwasawaT}$ applied to $p$ is a subgroup of the set of projective special linear groups of $x_{1}$ and $F$ defined as the map of $\operatorname{mk'}$ applied to the center of the set of special linear groups of $x_{1}$ and $F$ and $\operatorname{lineStab}$ applied to the submodule of $p$.
Projectivization.SubspacestructureMathlib.LinearAlgebra.Projectivization.Subspace, typeWording
subspace of K and V (from the name)
English
Let $K$ and $V$ be sets. Then the subspaces of $K$ and $V$ are a basic type.
Projectivization.Subspace.carrierdefMathlib.LinearAlgebra.Projectivization.Subspace, function or constantWording
the carrier of self (from the name)
English
Let $\mathrm{self}$ be a subspace of $K$ and $V$. Then the carrier of $\mathrm{self}$ is an element of the power set of the set of projectivizations of $K$ and $V$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
Projectivization.Subspace.gidefMathlib.LinearAlgebra.Projectivization.Subspace, function or constantEnglish
$\operatorname{gi}$ is a Galois insertion of $\operatorname{span}$ and $\operatorname{instSetLike}$.
Projectivization.Subspace.spandefMathlib.LinearAlgebra.Projectivization.Subspace, function or constantWording
the span of S (from the docstring)
English
Let $S$ be an element of the power set of the set of projectivizations of $K$ and $V$. Then the span of $S$ is a subspace of $K$ and $V$.
Projectivization.Subspace.submoduledefMathlib.LinearAlgebra.Projectivization.Subspace, function or constantWording
the submodule corresponding to a projective subspace (from the docstring)
English
The submodule corresponding to a projective subspace is an order isomorphism of the set of subspaces of $K$ and $V$ and the set of submodules of $K$ and $V$.
Submodule.projectivizationdefMathlib.LinearAlgebra.Projectivization.Subspace, function or constantWording
the projective subspace corresponding to a submodule (from the docstring)
English
The projective subspace corresponding to a submodule is an order isomorphism of the set of submodules of $K$ and $V$ and the set of subspaces of $K$ and $V$ defined as the inverse of the submodule corresponding to a projective subspace.