LinearEquiv.congrQuadraticMapdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the congruence quadratic map of e (from the name)
English
Let $e$ be a linear equivalence of $N$ and $P$. Then the congruence quadratic map of $e$ is a linear equivalence of the set of quadratic maps of $M$ and $N$ and the set of quadratic maps of $M$ and $P$.
LinearMap.BilinMap.toQuadraticMapdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the quadratic map of B (from the name)
English
Let $B$ be a bilinear map of $M$ and $N$. Then the quadratic map of $B$ is a quadratic map of $M$ and $N$.
LinearMap.BilinMap.toQuadraticMapAddMonoidHomdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the quadratic map additive monoid homomorphism of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the quadratic map additive monoid homomorphism of $R$ and $M$ is an additive monoid homomorphism of the set of bilinear maps of $M$ and $N$ and the set of quadratic maps of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toQuadraticMap}$ and $\mathrm{LinearMap\_\_BilinMap\_\_toQuadraticMap\_zero}$ applied to $R$ and $M$ and $\mathrm{LinearMap\_\_BilinMap\_\_toQuadraticMap\_add}$.
LinearMap.BilinMap.toQuadraticMapLinearMapdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the quadratic map linear map of R and M (from the name)
English
Let $S$, $R$ and $M$ be sets. Then the quadratic map linear map of $R$ and $M$ is a linear map of the set of bilinear maps of $M$ and $N$ and the set of quadratic maps of $M$ and $N$.
LinearMap.compQuadraticMapdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the composition quadratic map of f and Q (from the name)
English
Let $f$ be a linear map of $N$ and $P$. Let $Q$ be a quadratic map of $M$ and $N$. Then the composition quadratic map of $f$ and $Q$ is a quadratic map of $M$ and $P$.
LinearMap.compQuadraticMap'defMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the composition quadratic map of f and Q (from the name)
English
Let $f$ be a linear map of $N$ and $P$. Let $Q$ be a quadratic map of $M$ and $N$. Then the composition quadratic map of $f$ and $Q$ is a quadratic map of $M$ and $P$ defined as the composition quadratic map of $f$ and $\operatorname{restrictScalars}$ applied to $Q$.
QuadraticMapstructureMathlib.LinearAlgebra.QuadraticForm.Basic, typeWording
quadratic map of M and N (from the name)
English
Let $R$, $M$ and $N$ be sets. Then the quadratic maps of $M$ and $N$ are a basic type.
QuadraticMap.AnisotropicdefMathlib.LinearAlgebra.QuadraticForm.Basic, predicateWording
Q is anisotropic (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Then $Q$ is anisotropic, if for all elements $x_{5}$ of $M$, if $\EqtMACRoH {Q (x_{5})}{0}$, then $\EqtMACRoH {x_{5}}{0}$.
QuadraticMap.IsOrthodefMathlib.LinearAlgebra.QuadraticForm.Basic, predicateEnglish
Let $Q$ be a quadratic map of $M$ and $N$. Let $x_{5}$ and $y$ be elements of $M$. Then $\operatorname{IsOrtho}$ holds for $Q$, $x_{5}$ and $y$, if $\EqtMACRoH {Q (x_{5} + y)}{Q (x_{5})+ Q (y)}$.
QuadraticMap.PosDefdefMathlib.LinearAlgebra.QuadraticForm.Basic, predicateWording
x7 is a positive part (from the name)
English
Let $x_{7}$ be a quadratic map of $M$ and $N$. Then $x_{7}$ is a positive part, if for all elements $x_{8}$ of $M$, if $x_{8} \neq 0$, then $0 < x_{7} (x_{8})$.
QuadraticMap.associateddefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
$\operatorname{associated}$ is a linear map of the set of quadratic maps of $M$ and $N$ and the set of bilinear maps of $M$ and $N$ defined as $\operatorname{associatedHom}$ applied to $R$.
QuadraticMap.associated'defMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
$\operatorname{associated'}$ is a linear map of the set of quadratic maps of $M$ and $N$ and the set of bilinear maps of $M$ and $N$ defined as $\operatorname{associatedHom}$ applied to $\Integer$.
QuadraticMap.associatedHomdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
Let $S$ be a set. Then $\operatorname{associatedHom}$ applied to $S$ is a linear map of the set of quadratic maps of $M$ and $N$ and the set of bilinear maps of $M$ and $N$.
QuadraticMap.basisReprdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the basis representation of Q and v (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Let $v$ be a basis of $R$ and $M$. Then the basis representation of $Q$ and $v$ is a quadratic map of the set of functions from elements of $x_{5}$ to elements of $R$ and $N$ defined as the composition of $Q$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence function of $v$.
QuadraticMap.compdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the composition of Q and f (from the name)
English
Let $Q$ be a quadratic map of $N$ and $P$. Let $f$ be a linear map of $M$ and $N$. Then the composition of $Q$ and $f$ is a quadratic map of $M$ and $P$.
QuadraticMap.copydefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the copy of Q and h (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Let $\mathrm{Q'}$ be a function from elements of $M$ to elements of $N$ such that $\mathrm{Q'}$ is equal to $\operatorname{coe}$ applied to $Q$. Then the copy of $Q$ and $\mathrm{Q'}$ is a quadratic map of $M$ and $N$.
QuadraticMap.evalAddMonoidHomdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the evaluation additive monoid homomorphism of m (from the name)
English
Let $m$ be an element of $M$. Then the evaluation additive monoid homomorphism of $m$ is an additive monoid homomorphism of the set of quadratic maps of $M$ and $N$ and $N$ defined as the composition of the evaluation additive monoid homomorphism of the function that maps $x_{5}$ to $N$ and $m$ and the coercion additive monoid homomorphism of $M$ and $N$.
QuadraticMap.linMulLindefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
Let $f$ and $g$ be linear maps of $M$ and $A$. Then $\operatorname{linMulLin}$ applied to $f$ and $g$ is a quadratic map of $M$ and $A$.
QuadraticMap.ofPolardefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the quadratic map of toFun (from the name)
English
Let $\mathrm{toFun}$ be a function from elements of $M$ to elements of $N$ such that for all elements $a_{1}$ of $R$, for all elements $x_{7}$ of $M$, $\EqtMACRoH {\mathrm{toFun} (\HSMulhSMulMACRoAL {a_{1}}{x_{7}})}{\HSMulhSMulMACRoAL {(a_{1} \times a_{1})}{\mathrm{toFun} (x_{7})}}$, for all elements $x_{6}$ of $M$, for all elements $\mathrm{x'}$ of $M$, for all elements $y_{1}$ of $M$, $\EqtMACRoH {\operatorname{polar} (\mathrm{toFun} , x_{6} + \mathrm{x'} , y_{1})}{\operatorname{polar} (\mathrm{toFun} , x_{6} , y_{1})+ \operatorname{polar} (\mathrm{toFun} , \mathrm{x'} , y_{1})}$ and for all elements $a$ of $R$, for all elements $x_{5}$ of $M$, for all elements $y$ of $M$, $\EqtMACRoH {\operatorname{polar} (\mathrm{toFun} , \HSMulhSMulMACRoAL {a}{x_{5}}, y)}{\HSMulhSMulMACRoAL {a}{\operatorname{polar} (\mathrm{toFun} , x_{5} , y)}}$. Then the quadratic map of $\mathrm{toFun}$ is a quadratic map of $M$ and $N$.
QuadraticMap.polardefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{2}$ and $y$ be elements of $M$. Then $\operatorname{polar}$ applied to $f$, $x_{2}$ and $y$ is an element of $N$ defined as $f (x_{2} + y)- f (x_{2})- f (y)$.
QuadraticMap.polarBilindefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the polar bilinear of Q (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Then the polar bilinear of $Q$ is a bilinear map of $M$ and $N$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $R$, $\operatorname{polar}$ applied to $\operatorname{coe}$ applied to $Q$, $\mathrm{QuadraticMap\_\_polar\_add\_left}$ applied to $Q$, $\mathrm{QuadraticMap\_\_polar\_smul\_left}$ applied to $Q$, $\mathrm{QuadraticMap\_\_polar\_add\_right}$ applied to $Q$ and $\mathrm{QuadraticMap\_\_polar\_smul\_right}$ applied to $Q$.
QuadraticMap.polarSym2defMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the polar symmetric power of f and x2 (from the name)
English
Let $f$ be a function from elements of $M$ to elements of $N$. Let $x_{2}$ be a symmetric square of $M$. Then the polar symmetric power of $f$ and $x_{2}$ is an element of $N$ defined as $\operatorname{lift}$ applied to $\operatorname{polar}$ applied to $f$ and $x_{2}$.
QuadraticMap.projdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the projection of i and j (from the name)
English
Let $i$ and $j$ be elements of $n$. Then the projection of $i$ and $j$ is a quadratic map of the set of functions from elements of $n$ to elements of $A$ and $A$ defined as $\operatorname{linMulLin}$ applied to the projection of $i$ and the projection of $j$.
QuadraticMap.restrictdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
Let $Q$ be a quadratic map of $M$ and $N$. Let $V$ be a submodule of $R$ and $M$. Then $\operatorname{restrict}$ applied to $Q$ and $V$ is a quadratic map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {V}{x_{5}})}$ and $N$.
QuadraticMap.restrictScalarsdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantEnglish
Let $Q$ be a quadratic map of $M$ and $N$. Then $\operatorname{restrictScalars}$ applied to $Q$ is a quadratic map of $M$ and $N$.
QuadraticMap.sqdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the square (from the name)
English
The square is a quadratic map of $A$ and $A$ defined as $\operatorname{linMulLin}$ applied to the identity and the identity.
QuadraticMap.toFundefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the quadratic map of self and x5 (from the name)
English
Let $\mathrm{self}$ be a quadratic map of $M$ and $N$. Let $x_{5}$ be an element of $M$. Then the quadratic map of $\mathrm{self}$ and $x_{5}$ is an element of $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.
QuadraticMap.weightedSumSquaresdefMathlib.LinearAlgebra.QuadraticForm.Basic, function or constantWording
the weighted sum square of R and w (from the name)
English
Let $R$ be a set. Let $w$ be a function from elements of $x_{1}$ to elements of $S$. Then the weighted sum square of $R$ and $w$ is a quadratic map of the set of functions from elements of $x_{1}$ to elements of $R$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {w (i)}{\operatorname{proj} (i , i)})}$.
QuadraticMap.toBilindefMathlib.LinearAlgebra.QuadraticForm.Basis, function or constantWording
the bilinear of Q and bm (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Let $\mathrm{bm}$ be a basis of $R$ and $M$. Then the bilinear of $Q$ and $\mathrm{bm}$ is a bilinear map of $M$ and $N$ defined as $\operatorname{constr}$ applied to $\mathrm{bm}$, $R$ and the function that maps $i_{1}$ to $\operatorname{constr}$ applied to $\mathrm{bm}$, $R$ and the function that maps $j$ to $\iteMACRoG {(\EqtMACRoH {i_{1}}{j})}{Q (\mathrm{bm} (i_{1}))}{(\iteMACRoG {\mathrm{Lt} (i_{1} , j)}{\operatorname{polar} (\operatorname{coe} (Q), \mathrm{bm} (i_{1}), \mathrm{bm} (j))}{0})}$.
QuadraticMap.toBilinHomdefMathlib.LinearAlgebra.QuadraticForm.Basis, function or constantWording
the bilinear homomorphism of S and bm (from the name)
English
Let $S$ be a set. Let $\mathrm{bm}$ be a basis of $R$ and $M$. Then the bilinear homomorphism of $S$ and $\mathrm{bm}$ is a linear map of the set of quadratic maps of $M$ and $N$ and the set of bilinear maps of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $Q$ to the bilinear of $Q$ and $\mathrm{bm}$ and $\mathrm{QuadraticMap\_\_add\_toBilin}$ applied to $\mathrm{bm}$ and $\mathrm{QuadraticMap\_\_smul\_toBilin}$ applied to $S$ and $\mathrm{bm}$.
LinearMap.dualProddefMathlib.LinearAlgebra.QuadraticForm.Dual, function or constantWording
the dual product of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the dual product of $R$ and $M$ is a bilinear form of $R$ and $\mathrm{Prod}$ applied to the set of duals of $R$ and $M$ and $M$ defined as the sum of the complement of the composition of $\mathrm{LinearMap\_\_apply\_u2097\_}$ and the second component of the set of duals of $R$ and $M$ and $M$ and the first component of the set of duals of $R$ and $M$ and $M$ and the flip of the complement of the composition of $\mathrm{LinearMap\_\_apply\_u2097\_}$ and the second component of the set of duals of $R$ and $M$ and $M$ and the first component of the set of duals of $R$ and $M$ and $M$.
QuadraticMap.IsometrystructureMathlib.LinearAlgebra.QuadraticForm.Isometry, typeWording
isometry of x9 and x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $N$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $N$. Then the isometries of $x_{9}$ and $x_{10}$ are a basic type.
QuadraticMap.Isometry.compdefMathlib.LinearAlgebra.QuadraticForm.Isometry, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an isometry of $x_{13}$ and $x_{14}$. Let $f$ be an isometry of $x_{12}$ and $x_{13}$. Then the composition of $g$ and $f$ is an isometry of $x_{12}$ and $x_{14}$.
QuadraticMap.Isometry.iddefMathlib.LinearAlgebra.QuadraticForm.Isometry, function or constantWording
the identity isometry of Q (from the docstring)
English
Let $Q$ be a quadratic map of $M$ and $N$. Then the identity isometry of $Q$ is an isometry of $Q$ and $Q$.
QuadraticMap.Isometry.ofEqdefMathlib.LinearAlgebra.QuadraticForm.Isometry, function or constantWording
the isometry of h (from the name)
English
Assume that $\EqtMACRoH {x_{6}}{x_{7}}$. Then the isometry of $h$ is an isometry of $x_{6}$ and $x_{7}$.
QuadraticMap.EquivalentdefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, predicateWording
x9 is equivalent to x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $N$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $N$. Then $x_{9}$ is equivalent to $x_{10}$, if $\mathrm{Nonempty}$ holds for the set of isometry equivalences of $x_{9}$ and $x_{10}$.
QuadraticMap.IsometryEquivstructureMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, typeWording
isometry equivalence of x9 and x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $N$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $N$. Then the isometry equivalences of $x_{9}$ and $x_{10}$ are a basic type.
QuadraticMap.IsometryEquiv.refldefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the identity of Q (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Then the identity of $Q$ is an isometry equivalence of $Q$ and $Q$.
QuadraticMap.IsometryEquiv.symmdefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the inverse isometric equivalence of f (from the docstring)
English
Let $f$ be an isometry equivalence of $x_{9}$ and $x_{10}$. Then the inverse isometric equivalence of $f$ is an isometry equivalence of $x_{10}$ and $x_{9}$.
QuadraticMap.IsometryEquiv.toIsometrydefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the isometry of g (from the name)
English
Let $g$ be an isometry equivalence of $x_{9}$ and $x_{10}$. Then the isometry of $g$ is an isometry of $x_{9}$ and $x_{10}$.
QuadraticMap.IsometryEquiv.transdefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the composition of f and g (from the name)
English
Let $f$ be an isometry equivalence of $x_{12}$ and $x_{13}$. Let $g$ be an isometry equivalence of $x_{13}$ and $x_{14}$. Then the composition of $f$ and $g$ is an isometry equivalence of $x_{12}$ and $x_{14}$.
QuadraticMap.isometryEquivBasisReprdefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the isometry equivalence basis representation of Q and v (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Let $v$ be a basis of $R$ and $M$. Then the isometry equivalence basis representation of $Q$ and $v$ is an isometry equivalence of $Q$ and the basis representation of $Q$ and $v$ defined as the isometry equivalence of $Q$ and the inverse of the equivalence function of $v$.
QuadraticMap.isometryEquivOfCompLinearEquivdefMathlib.LinearAlgebra.QuadraticForm.IsometryEquiv, function or constantWording
the isometry equivalence of Q and f (from the name)
English
Let $Q$ be a quadratic map of $M$ and $N$. Let $f$ be a linear equivalence of $x$ and $M$. Then the isometry equivalence of $Q$ and $f$ is an isometry equivalence of $Q$ and the composition of $Q$ and $\operatorname{toLinearMap}$ applied to $f$.
QuadraticMap.Isometry.fstdefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the first component of x1 and x9 (from the name)
English
Let $x_{1}$ be a set. Let $x_{9}$ be a quadratic map of $x$ and $P$. Then the first component of $x_{1}$ and $x_{9}$ is an isometry of the product of $x_{9}$ and $0$ and $x_{9}$.
QuadraticMap.Isometry.inldefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the left injection of x9 and x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $P$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $P$. Then the left injection of $x_{9}$ and $x_{10}$ is an isometry of $x_{9}$ and the product of $x_{9}$ and $x_{10}$.
QuadraticMap.Isometry.inrdefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the right injection of x9 and x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $P$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $P$. Then the right injection of $x_{9}$ and $x_{10}$ is an isometry of $x_{10}$ and the product of $x_{9}$ and $x_{10}$.
QuadraticMap.Isometry.projdefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the projection of i and Q (from the name)
English
Let $i$ be an element of $x$. Let $Q$ be a quadratic map of $x_{1}$ applied to $i$ and $P$. Then the projection of $i$ and $Q$ is an isometry of the product of $\operatorname{single}$ applied to $i$ and $Q$ and $Q$.
QuadraticMap.Isometry.singledefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantEnglish
Let $Q$ be a function from elements $i_{1}$ of $x$ to quadratic maps of $x_{1}$ applied to $i_{1}$ and $P$. Let $i$ be an element of $x$. Then $\operatorname{single}$ applied to $i_{1}$, $Q$ and $i$ is an isometry of $Q$ applied to $i$ and the product of $Q$ defined as the function that maps $i$ to $\operatorname{mk}$ applied to $\operatorname{single}$ applied to $R$, $x_{1}$ and $Q$, $\mathrm{QuadraticMap\_\_pi\_apply\_single}$ applied to $i_{1}$ and $Q$ and $i$.
QuadraticMap.Isometry.snddefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the second component of x and x9 (from the name)
English
Let $x$ be a set. Let $x_{9}$ be a quadratic map of $x_{1}$ and $P$. Then the second component of $x$ and $x_{9}$ is an isometry of the product of $0$ and $x_{9}$ and $x_{9}$.
QuadraticMap.IsometryEquiv.pidefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the product of e (from the name)
English
Let $e$ be a function from elements $i$ of $x$ to isometry equivalences of $Q$ applied to $i$ and $\mathrm{Q'}$ applied to $i$. Then the product of $i$ is an isometry equivalence of the product of $Q$ and the product of $\mathrm{Q'}$.
QuadraticMap.IsometryEquiv.proddefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the product of x19 and x20 (from the name)
English
Let $x_{19}$ be an isometry equivalence of $x_{15}$ and $x_{17}$. Let $x_{20}$ be an isometry equivalence of $x_{16}$ and $x_{18}$. Then the product of $x_{19}$ and $x_{20}$ is an isometry equivalence of the product of $x_{15}$ and $x_{16}$ and the product of $x_{17}$ and $x_{18}$.
QuadraticMap.IsometryEquiv.prodCommdefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantEnglish
Let $x_{9}$ be a quadratic map of $x$ and $P$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $P$. Then $\operatorname{prodComm}$ applied to $x_{9}$ and $x_{10}$ is an isometry equivalence of the product of $x_{9}$ and $x_{10}$ and the product of $x_{10}$ and $x_{9}$.
QuadraticMap.IsometryEquiv.prodProdProdCommdefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantEnglish
Let $x_{15}$ be a quadratic map of $x$ and $P$. Let $x_{16}$ be a quadratic map of $x_{1}$ and $P$. Let $x_{17}$ be a quadratic map of $x_{2}$ and $P$. Let $x_{18}$ be a quadratic map of $x_{3}$ and $P$. Then $\operatorname{prodProdProdComm}$ applied to $x_{15}$, $x_{16}$, $x_{17}$ and $x_{18}$ is an isometry equivalence of the product of the product of $x_{15}$ and $x_{16}$ and the product of $x_{17}$ and $x_{18}$ and the product of the product of $x_{15}$ and $x_{17}$ and the product of $x_{16}$ and $x_{18}$.
QuadraticMap.pidefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the product of Q (from the name)
English
Let $Q$ be a function from elements $i_{1}$ of $x$ to quadratic maps of $x_{1}$ applied to $i_{1}$ and $P$. Then the product of $i_{1}$ is a quadratic map of the set of functions from elements $i$ of $x$ to elements of $x_{1}$ applied to $i$ and $P$ defined as the function that maps $Q$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (i_{1} (i), \operatorname{proj} (i))}{Q}$.
QuadraticMap.proddefMathlib.LinearAlgebra.QuadraticForm.Prod, function or constantWording
the product of x9 and x10 (from the name)
English
Let $x_{9}$ be a quadratic map of $x$ and $P$. Let $x_{10}$ be a quadratic map of $x_{1}$ and $P$. Then the product of $x_{9}$ and $x_{10}$ is a quadratic map of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $P$ defined as the sum of the composition of $x_{9}$ and the first component of $x$ and $x_{1}$ and the composition of $x_{10}$ and the second component of $x$ and $x_{1}$.
CategoryTheory.Iso.toIsometryEquivdefMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantWording
the isometry equivalence of i (from the name)
English
Let $i$ be an isomorphism of $X$ and $Y$. Then the isometry equivalence of $i$ is an isometry equivalence of the quadratic form associated with the module of $X$ and the quadratic form associated with the module of $Y$.
QuadraticModuleCatstructureMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, typeWording
quadratic module category of R (from the name)
English
Let $R$ be a set. Then the quadratic module categories of $R$ are a basic type.
QuadraticModuleCat.HomstructureMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, typeWording
homomorphism of V and W (from the name)
English
Let $V$ and $W$ be quadratic module categories of $R$. Then the homomorphisms of $V$ and $W$ are a basic type.
QuadraticModuleCat.Hom.toIsometrydefMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantWording
the isometry of f (from the name)
English
Let $f$ be a homomorphism of $X$ and $Y$. Then the isometry of $f$ is an isometry of the quadratic form associated with the module of $X$ and the quadratic form associated with the module of $Y$ defined as the homomorphism of $f$.
QuadraticModuleCat.Hom.toIsometry'defMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantWording
the underlying isometry of self (from the docstring)
English
Let $\mathrm{self}$ be a homomorphism of $V$ and $W$. Then the underlying isometry of $\mathrm{self}$ is an isometry of the quadratic form associated with the module of $V$ and the quadratic form associated with the module of $W$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
QuadraticModuleCat.ofdefMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantEnglish
Let $Q$ be a quadratic form of $R$ and $X$. Then $\operatorname{of}$ applied to $Q$ is a quadratic module category of $R$ defined as $\operatorname{mk}$ applied to $\operatorname{of}$ applied to $R$ and $X$ and $Q$.
QuadraticModuleCat.ofHomdefMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantWording
the quadratic module category of f (from the name)
English
Let $f$ be an isometry of $x_{5}$ and $x_{6}$. Then the quadratic module category of $f$ is a homomorphism of $\operatorname{of}$ applied to $x_{5}$ and $\operatorname{of}$ applied to $x_{6}$ defined as the concrete category of $f$.
QuadraticModuleCat.ofIsodefMathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat, function or constantWording
the quadratic module category of e (from the name)
English
Let $e$ be an isometry equivalence of $x_{5}$ and $x_{6}$. Then the quadratic module category of $e$ is an isomorphism of $\operatorname{of}$ applied to $x_{5}$ and $\operatorname{of}$ applied to $x_{6}$.
QuadraticMap.NondegeneratestructureMathlib.LinearAlgebra.QuadraticForm.Radical, predicateEnglish
We can say that $\operatorname{Nondegenerate}$.
QuadraticMap.liftdefMathlib.LinearAlgebra.QuadraticForm.Radical, function or constantWording
the lift of Q and N (from the name)
English
Let $Q$ be a quadratic map of $M$ and $P$. Let $N$ be a submodule of $R$ and $M$ such that $N$ is less than or equal to the radical of $Q$. Then the lift of $Q$ and $N$ is a quadratic map of the set of quotients of $M$ and $N$ and $P$.
QuadraticMap.radicaldefMathlib.LinearAlgebra.QuadraticForm.Radical, function or constantWording
the radical of Q (from the docstring)
English
Let $Q$ be a quadratic map of $M$ and $P$. Then the radical of $Q$ is a submodule of $R$ and $M$.
sigNegdefMathlib.LinearAlgebra.QuadraticForm.Signature, function or constantEnglish
Let $Q$ be a quadratic form of $R$ and $M$. Then $\mathrm{sigNeg}$ applied to $Q$ is a natural number defined as $\mathrm{sigPos}$ applied to $\operatorname{neg}$ applied to $Q$.
sigPosdefMathlib.LinearAlgebra.QuadraticForm.Signature, function or constantEnglish
Let $Q$ be a quadratic form of $R$ and $M$. Then $\mathrm{sigPos}$ applied to $Q$ is a natural number.
QuadraticMap.tensorDistribdefMathlib.LinearAlgebra.QuadraticForm.TensorProduct, function or constantEnglish
Let $R$ and $A$ be sets. Then $\operatorname{tensorDistrib}$ applied to $R$ and $A$ is a linear map of the set of tensor products of the set of quadratic maps of $x$ and $x_{2}$ and the set of quadratic maps of $x_{1}$ and $x_{3}$ and the set of quadratic maps of the set of tensor products of $x$ and $x_{1}$ and the set of tensor products of $x_{2}$ and $x_{3}$ defined as the composition of the quadratic map linear map of $A$ and the set of tensor products of $x$ and $x_{1}$ and the composition of $\operatorname{tensorDistrib}$ applied to $R$ and $A$ and the map of $\operatorname{associated}$ and $\operatorname{associated}$.
QuadraticMap.tmuldefMathlib.LinearAlgebra.QuadraticForm.TensorProduct, function or constantEnglish
Let $x_{18}$ be a quadratic map of $x$ and $x_{2}$. Let $x_{19}$ be a quadratic map of $x_{1}$ and $x_{3}$. Then $\operatorname{tmul}$ applied to $x_{18}$ and $x_{19}$ is a quadratic map of the set of tensor products of $x$ and $x_{1}$ and the set of tensor products of $x_{2}$ and $x_{3}$ defined as $\operatorname{tensorDistrib}$ applied to $R$, $A$ and $\operatorname{tmul}$ applied to $R$, $x_{18}$ and $x_{19}$.
QuadraticMap.Isometry.tmuldefMathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries, function or constantEnglish
Let $f$ be an isometry of $x_{14}$ and $x_{15}$. Let $g$ be an isometry of $x_{16}$ and $x_{17}$. Then $\operatorname{tmul}$ applied to $f$ and $g$ is an isometry of $\operatorname{tmul}$ applied to $x_{14}$ and $x_{16}$ and $\operatorname{tmul}$ applied to $x_{15}$ and $x_{17}$ defined as $\operatorname{mk}$ applied to the tensor product of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{toLinearMap}$ applied to $g$ and $\mathrm{QuadraticForm\_\_tmul\_tensorMap\_apply}$ applied to $f$ and $g$.
Submodule.Quotient.equivdefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the equivalence of Q and f (from the name)
English
Let $P$ be a submodule of $R$ and $M$. Let $Q$ be a submodule of $x_{1}$ and $N$. Let $f$ be a linear equivalence of $M$ and $N$ such that the map of $\operatorname{toLinearMap}$ applied to $f$ and $P$ is equal to $Q$. Then the equivalence of $Q$ and $f$ is a linear equivalence of the set of quotients of $M$ and $P$ and the set of quotients of $N$ and $Q$.
Submodule.Quotient.restrictScalarsEquivdefMathlib.LinearAlgebra.Quotient.Basic, function or constantEnglish
Let $S$ be a set. Let $P$ be a submodule of $R$ and $M$. Then $\operatorname{restrictScalarsEquiv}$ applied to $S$ and $P$ is a linear equivalence of the set of quotients of $M$ and $\operatorname{restrictScalars}$ applied to $S$ and $P$ and the set of quotients of $M$ and $P$.
Submodule.comapMkQOrderEmbeddingdefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the preimage order embedding of p (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Then the preimage order embedding of $p$ is an order embedding of the set of submodules of $R$ and the set of quotients of $M$ and $p$ and the set of submodules of $R$ and $M$ defined as the composition of the relation embedding of the preimage relation isomorphism of $p$ and the induced relation of the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Leq} (x_{3} , x_{4})$ and the function that maps $x_{5}$ to $\MembershipmemMACRoT {\operatorname{Ici} (p)}{x_{5}}$.
Submodule.comapMkQRelIsodefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the preimage relation isomorphism of p (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Then the preimage relation isomorphism of $p$ is an order isomorphism of the set of submodules of $R$ and the set of quotients of $M$ and $p$ and the set of elements of $\operatorname{Ici}$ applied to $p$.
Submodule.factordefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the factor of H (from the name)
English
Assume that $p \leq \mathrm{p'}$. Then the factor of $H$ is a linear map of the set of quotients of $M$ and $p$ and the set of quotients of $M$ and $\mathrm{p'}$ defined as the map from the quotient of $p$.
Submodule.liftQdefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the lift of p and f (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Let $f$ be a linear map of $M$ and $x_{4}$ such that $p$ is less than or equal to the kernel of $f$. Then the lift of $p$ and $f$ is a linear map of the set of quotients of $M$ and $p$ and $x_{4}$.
Submodule.liftQSpanSingletondefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the lift span singleton of x9 and f (from the name)
English
Let $x_{9}$ be an element of $M$. Let $f$ be a linear map of $M$ and $x_{4}$ such that $\EqtMACRoH {f (x_{9})}{0}$. Then the lift span singleton of $x_{9}$ and $f$ is a linear map of the set of quotients of $M$ and the span of $R$ and $\operatorname{singleton}$ applied to $x_{9}$ and $x_{4}$.
Submodule.mapQdefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the map from the quotient of p (from the docstring)
English
Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $x_{3}$ and $x_{4}$. Let $f$ be a linear map of $M$ and $x_{4}$ such that $p$ is less than or equal to the preimage of $f$ and $q$. Then the map from the quotient of $p$ is a linear map of the set of quotients of $M$ and $p$ and the set of quotients of $x_{4}$ and $q$.
Submodule.mapQLineardefMathlib.LinearAlgebra.Quotient.Basic, function or constantEnglish
Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $R$ and $x$. Then $\operatorname{mapQLinear}$ applied to $p$ and $q$ is a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{compatibleMaps} (p , q)}{x_{6}})}$ and the set of linear maps of the set of quotients of $M$ and $p$ and the set of quotients of $x$ and $q$.
Submodule.quotEquivOfEqBotdefMathlib.LinearAlgebra.Quotient.Basic, function or constantWording
the quotient equivalence of p and hp (from the name)
English
Let $p$ be a submodule of $R$ and $M$ such that $p$ is equal to the bottom. Then the quotient equivalence of $p$ and $\mathrm{hp}$ is a linear equivalence of the set of quotients of $M$ and $p$ and $M$.
LinearMap.IsRefl.liftQ₂defMathlib.LinearAlgebra.Quotient.Bilinear, function or constantWording
the lift of f and N (from the name)
English
Let $f$ be a linear map of $M$ and the set of linear maps of $M$ and $P$. Let $N$ be a submodule of $R$ and $M$. Assume that $f$ is an identity. Assume that $N$ is less than or equal to the kernel of $f$. Then the lift of $f$ and $N$ is a linear map of the set of quotients of $M$ and $N$ and the set of linear maps of the set of quotients of $M$ and $N$ and $P$.
LinearMap.liftQ₂defMathlib.LinearAlgebra.Quotient.Bilinear, function or constantWording
the lift of #2 and #3 (from the name)
English
Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Let $\mathrm{N'}$ be a submodule of $S$ and $N$. Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$ such that $\mathrm{M'}$ is less than or equal to the kernel of $f$ and $\mathrm{N'}$ is less than or equal to the kernel of the flip of $f$. Then the lift of $\mathrm{N'}$ and $f$ is a linear map of the set of quotients of $M$ and $\mathrm{M'}$ and the set of linear maps of the set of quotients of $N$ and $\mathrm{N'}$ and $P$.
Submodule.Quotient.mkdefMathlib.LinearAlgebra.Quotient.Defs, function or constantEnglish
Let $x_{3}$ be an element of $M$. Then $\operatorname{mk}$ applied to $x_{3}$ is a quotient of $M$ and $p$ defined as $\operatorname{mk''}$ applied to $x_{3}$.
Submodule.mkQdefMathlib.LinearAlgebra.Quotient.Defs, function or constantEnglish
Let $p$ be a submodule of $R$ and $M$. Then $\operatorname{mkQ}$ applied to $p$ is a linear map of $M$ and the set of quotients of $M$ and $p$.
Submodule.quotEquivOfEqdefMathlib.LinearAlgebra.Quotient.Defs, function or constantWording
the quotient equivalence of p and h (from the name)
English
Let $p$ and $\mathrm{p'}$ be submodules of $R$ and $M$ such that $\EqtMACRoH {p}{\mathrm{p'}}$. Then the quotient equivalence of $p$ and $\mathrm{p'}$ is a linear equivalence of the set of quotients of $M$ and $p$ and the set of quotients of $M$ and $\mathrm{p'}$.
Submodule.piQuotientLiftdefMathlib.LinearAlgebra.Quotient.Pi, function or constantWording
the product quotient lift of i3 and q (from the name)
English
Let $p$ be a function from elements $i_{3}$ of $x$ to submodules of $R$ and $\mathrm{Ms}$ applied to $i_{3}$. Let $q$ be a submodule of $R$ and $N$. Let $f$ be a function from elements $i_{2}$ of $x$ to linear maps of $\mathrm{Ms}$ applied to $i_{2}$ and $N$ such that for all elements $i_{1}$ of $x$, $p$ applied to $i_{1}$ is less than or equal to the preimage of $f$ applied to $i_{1}$ and $q$. Then the product quotient lift of $p$ and $q$ is a linear map of the set of functions from elements $i$ of $x$ to quotients of $\mathrm{Ms}$ applied to $i$ and $p$ applied to $i$ and the set of quotients of $N$ and $q$ defined as the function that maps $f$ and $\mathrm{hf}$ to $\operatorname{lsum}$ applied to $R$, the function that maps $i_{3}$ to the set of quotients of $\mathrm{Ms}$ applied to $i_{3}$ and $i_{3}$ applied to $i_{3}$, $R$, the function that maps $i_{4}$ to the map from the quotient of $i_{3}$ applied to $i_{4}$, $f$ and $\mathrm{hf}$.
Submodule.quotientPidefMathlib.LinearAlgebra.Quotient.Pi, function or constantWording
the quotient of p (from the docstring)
English
Let $p$ be a function from elements $i_{2}$ of $x$ to submodules of $R$ and $\mathrm{Ms}$ applied to $i_{2}$. Then the quotient of $i_{2}$ is a linear equivalence of the set of quotients of the set of functions from elements $i$ of $x$ to elements of $\mathrm{Ms}$ applied to $i$ and the product of the universal set and $p$ and the set of functions from elements $i_{1}$ of $x$ to quotients of $\mathrm{Ms}$ applied to $i_{1}$ and $p$ applied to $i_{1}$ defined as the function that maps $p$ to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\mathrm{Submodule\_\_quotientPi\_aux\_\_toFun}$ and $\mathrm{Submodule\_\_quotientPi\_aux\_\_map\_add}$ applied to $i_{2}$ and $\mathrm{Submodule\_\_quotientPi\_aux\_\_map\_smul}$ applied to $i_{2}$, $\mathrm{Submodule\_\_quotientPi\_aux\_\_invFun}$ applied to $i_{2}$, $\mathrm{Submodule\_\_quotientPi\_aux\_\_left\_inv}$ applied to $i_{2}$, $\mathrm{Submodule\_\_quotientPi\_aux\_\_right\_inv}$ applied to $i_{2}$ and $p$.
Submodule.quotientPiLiftdefMathlib.LinearAlgebra.Quotient.Pi, function or constantWording
the quotient product lift of p and i4 (from the name)
English
Let $p$ be a function from elements $i_{4}$ of $x$ to submodules of $R$ and $\mathrm{Ms}$ applied to $i_{4}$. Let $f$ be a function from elements $i_{3}$ of $x$ to linear maps of $\mathrm{Ms}$ applied to $i_{3}$ and $\mathrm{Ns}$ applied to $i_{3}$ such that for all elements $i_{2}$ of $x$, $p$ applied to $i_{2}$ is less than or equal to the kernel of $f$ applied to $i_{2}$. Then the quotient product lift of $i_{4}$ and $p$ is a linear map of the set of quotients of the set of functions from elements $i$ of $x$ to elements of $\mathrm{Ms}$ applied to $i$ and the product of the universal set and $p$ and the set of functions from elements $i_{1}$ of $x$ to elements of $\mathrm{Ns}$ applied to $i_{1}$.
Submodule.quotientPi_aux.invFundefMathlib.LinearAlgebra.Quotient.Pi, function or constantWording
the inverse function of p and i2 (from the name)
English
Let $p$ be a function from elements $i_{2}$ of $x$ to submodules of $R$ and $\mathrm{Ms}$ applied to $i_{2}$. Let $x_{6}$ be a function from elements $i_{1}$ of $x$ to quotients of $\mathrm{Ms}$ applied to $i_{1}$ and $p$ applied to $i_{1}$. Then the inverse function of $i_{2}$ and $p$ is a quotient of the set of functions from elements $i$ of $x$ to elements of $\mathrm{Ms}$ applied to $i$ and the product of the universal set and $p$.
Submodule.quotientPi_aux.toFundefMathlib.LinearAlgebra.Quotient.Pi, function or constantWording
the quotient product of i2 and x4 (from the name)
English
Let $p$ be a function from elements $i_{2}$ of $x$ to submodules of $R$ and $\mathrm{Ms}$ applied to $i_{2}$. Let $x_{4}$ be a quotient of the set of functions from elements $i_{1}$ of $x$ to elements of $\mathrm{Ms}$ applied to $i_{1}$ and the product of the universal set and $p$. Let $i$ be an element of $x$. Then the quotient product of $p$ and $x_{4}$ is a quotient of $\mathrm{Ms}$ applied to $i$ and $p$ applied to $i$.
Module.RaydefMathlib.LinearAlgebra.Ray, typeWording
ray of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a ray of $R$ and $M$ is an element of the function that maps $R$ and $M$ to $\mathrm{Quotient}$ applied to $\operatorname{Setoid}$ applied to $R$ and $M$.
Module.Ray.mapdefMathlib.LinearAlgebra.Ray, function or constantWording
the map of e (from the name)
English
Let $e$ be a linear equivalence of $M$ and $N$. Then the map of $e$ is an equivalence from the set of rays of $R$ and $M$ to the set of rays of $R$ and $N$.
Module.Ray.someRayVectordefMathlib.LinearAlgebra.Ray, function or constantEnglish
Let $x_{4}$ be a ray of $R$ and $M$. Then $\operatorname{someRayVector}$ applied to $x_{4}$ is a ray vector of $R$ and $M$ defined as $\operatorname{out}$ applied to $x_{4}$.
Module.Ray.someVectordefMathlib.LinearAlgebra.Ray, function or constantEnglish
Let $x_{4}$ be a ray of $R$ and $M$. Then $\operatorname{someVector}$ applied to $x_{4}$ is an element of $M$ defined as $\operatorname{equiv}$ applied to $R$, $M$ and $\operatorname{someRayVector}$ applied to $x_{4}$.
RayVectordefMathlib.LinearAlgebra.Ray, typeWording
ray vector of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a ray vector of $R$ and $M$ is an element of the function that maps $R$ and $M$ to $\SubtypeSet {v}{\mathrm{Neq} (v , 0)}$.
RayVector.equivdefMathlib.LinearAlgebra.Ray, function or constantWording
the equivalence of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the equivalence of $R$ and $M$ is an equivalence from the set of ray vectors of $R$ and $M$ to $\SubtypeSet {v}{\mathrm{Neq} (v , 0)}$ defined as the identity of the set of ray vectors of $R$ and $M$.
RayVector.mapLinearEquivdefMathlib.LinearAlgebra.Ray, function or constantWording
the map linear equivalence of e (from the name)
English
Let $e$ be a linear equivalence of $M$ and $N$. Then the map linear equivalence of $e$ is an equivalence from the set of ray vectors of $R$ and $M$ to the set of ray vectors of $R$ and $N$.
SameRaydefMathlib.LinearAlgebra.Ray, predicateEnglish
Let $R$ be a set. Let $x_{4}$ and $x_{5}$ be elements of $M$. Then $\mathrm{SameRay}$ holds for $R$, $x_{4}$ and $x_{5}$, if $\EqtMACRoH {x_{4}}{0}$, $\EqtMACRoH {x_{5}}{0}$ or there exists an element $x_{6}$ of $R$ such that there exists an element $x_{7}$ of $R$ such that $0 < x_{6}$ and $0 < x_{7}$ and $\EqtMACRoH {\HSMulhSMulMACRoAL {x_{6}}{x_{4}}}{\HSMulhSMulMACRoAL {x_{7}}{x_{5}}}$.
rayOfNeZerodefMathlib.LinearAlgebra.Ray, function or constantWording
the ray of v (from the name)
English
Let $R$ be a set. Let $v$ be an element of $M$ such that $v \neq 0$. Then the ray of $v$ is a ray of $R$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{Setoid}$ applied to $R$ and $M$ and $\operatorname{symm}$ applied to the equivalence of $R$ and $M$ and $v$.
Module.preReflectiondefMathlib.LinearAlgebra.Reflection, function or constantWording
the reflection of x3 and f (from the name)
English
Let $x_{3}$ be an element of $M$. Let $f$ be a dual of $R$ and $M$. Then the reflection of $x_{3}$ and $f$ is an end of $R$ and $M$ defined as the difference between the identity and the right scalar multiple of $f$ and $x_{3}$.
Module.reflectiondefMathlib.LinearAlgebra.Reflection, function or constantWording
the reflection of h (from the name)
English
Assume that $\EqtMACRoH {f (x_{3})}{2}$. Then the reflection of $h$ is a linear equivalence of $M$ and $M$ defined as $\operatorname{mk}$ applied to the reflection of $x_{3}$ and $f$, $\operatorname{invFun}$ applied to the permutation of $\operatorname{coe}$ applied to the reflection of $x_{3}$ and $f$ and $\mathrm{Module\_\_involutive\_preReflection}$ applied to $h$, $\mathrm{Equiv\_\_left\_inv}$ applied to the permutation of $\operatorname{coe}$ applied to the reflection of $x_{3}$ and $f$ and $\mathrm{Module\_\_involutive\_preReflection}$ applied to $h$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the permutation of $\operatorname{coe}$ applied to the reflection of $x_{3}$ and $f$ and $\mathrm{Module\_\_involutive\_preReflection}$ applied to $h$.
RootPairing.BasestructureMathlib.LinearAlgebra.RootSystem.Base, typeWording
base of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the bases of $P$ are a basic type.
RootPairing.Base.IsPosdefMathlib.LinearAlgebra.RootSystem.Base, predicateWording
i is a positive part with respect to b (from the name)
English
Let $b$ be a base of $P$. Let $i$ be an element of $x$. Then $i$ is a positive part with respect to $b$, if $0$ is less than the height of $b$ and $i$.
RootPairing.Base.flipdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the flip of b (from the name)
English
Let $b$ be a base of $P$. Then the flip of $b$ is a base of the flip of $P$ defined as $\operatorname{mk}$ applied to the support of $b$, $\mathrm{RootPairing\_\_Base\_\_linearIndepOn\_coroot}$ applied to $b$, $\mathrm{RootPairing\_\_Base\_\_linearIndepOn\_root}$ applied to $b$, $\mathrm{RootPairing\_\_Base\_\_coroot\_mem\_or\_neg\_mem}$ applied to $b$ and $\mathrm{RootPairing\_\_Base\_\_root\_mem\_or\_neg\_mem}$ applied to $b$.
RootPairing.Base.heightdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the height of b and i (from the name)
English
Let $b$ be a base of $P$. Let $i$ be an element of $x$. Then the height of $b$ and $i$ is an element of $\Integer$ defined as $\FinsetSum {\operatorname{support} (b)}{j}{\operatorname{choose} (\mathrm{RootPairing\_\_Base\_\_exists\_root\_eq\_sum\_int} (b , i), j)}$.
RootPairing.Base.mapdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the map of b and e (from the name)
English
Let $b$ be a base of $P$. Let $e$ be an equivalence of $P$ and $x_{13}$. Then the map of $b$ and $e$ is a base of $x_{13}$.
RootPairing.Base.mkOfPairwiseLEZerodefMathlib.LinearAlgebra.RootSystem.Base, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$ such that $\mathrm{LinearIndepOn}$ holds for $R$, $\operatorname{coe}$ applied to the root of $P$ and $s$, $\operatorname{Pairwise}$ holds for $s$ and the function that maps $i_{2}$ and $j$ to $\mathrm{Leq} (\operatorname{pairingIn} (P , \Integer , i_{2} , j), 0)$, for all elements $i_{1}$ of $x$, $\operatorname{coroot}$ applied to $P$ and $i_{1}$ is an element of the span of $\Integer$ and the image of $\operatorname{coe}$ applied to the coroot of $P$ and $s$ and for all elements $i$ of $x$, $\operatorname{root}$ applied to $P$ and $i$ is an element of the span of $\Integer$ and the image of $\operatorname{coe}$ applied to the root of $P$ and $s$. Then $\operatorname{mkOfPairwiseLEZero}$ applied to $P$, $h_{4}$, $h_{5}$, $h_{6}$ and $h_{7}$ is a base of $P$.
RootPairing.Base.supportdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the support of self (from the name)
English
Let $\mathrm{self}$ be a base of $P$. Then the support of $\mathrm{self}$ is a finite set of $x$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RootPairing.Base.supportMapEquivdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the natural bijection between support of b and e (from the docstring)
English
Let $b$ be a base of $P$. Let $e$ be an equivalence of $P$ and $x_{13}$. Then the natural bijection between support of $b$ and $e$ is an element of $\EquivMACRoAE {(\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{15}})})}{(\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {\operatorname{support} (\operatorname{map} (b , e))}{x_{16}})})}$.
RootPairing.Base.toCoweightBasisdefMathlib.LinearAlgebra.RootSystem.Base, function or constantWording
the coweight basis of b (from the name)
English
Let $b$ be a base of $P$. Then the coweight basis of $b$ is a basis of $R$ and $N$ defined as $\operatorname{toWeightBasis}$ applied to the flip of $b$.
RootPairing.Base.toWeightBasisdefMathlib.LinearAlgebra.RootSystem.Base, function or constantEnglish
Let $b$ be a base of $P$. Then $\operatorname{toWeightBasis}$ applied to $b$ is a basis of $R$ and $M$.
RootPairing.Base.toWeightBasisIntdefMathlib.LinearAlgebra.RootSystem.Base, function or constantEnglish
Let $b$ be a base of $P$. Then $\operatorname{toWeightBasisInt}$ applied to $b$ is a basis of $\Integer$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{rootSpan} (P , \Integer)}{x_{7}})}$.
RootPairing.IsBalancedclassMathlib.LinearAlgebra.RootSystem.BaseChange, predicateWording
P is balanced (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is balanced.
RootPairing.restrictScalarsdefMathlib.LinearAlgebra.RootSystem.BaseChange, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $K$ be a set. Then $\operatorname{restrictScalars}$ applied to $P$ and $K$ is a root pairing of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{span} (K , \operatorname{range} (\operatorname{coe} (\operatorname{root} (P))))}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{span} (K , \operatorname{range} (\operatorname{coe} (\operatorname{coroot} (P))))}{x_{11}})}$ defined as $\operatorname{restrictScalars'}$ applied to $P$ and $K$.
RootPairing.restrictScalars'defMathlib.LinearAlgebra.RootSystem.BaseChange, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $K$ be a set. Then $\operatorname{restrictScalars'}$ applied to $P$ and $K$ is a root pairing of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{span} (K , \operatorname{range} (\operatorname{coe} (\operatorname{root} (P))))}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{span} (K , \operatorname{range} (\operatorname{coe} (\operatorname{coroot} (P))))}{x_{11}})}$.
RootPairing.restrictScalarsRatdefMathlib.LinearAlgebra.RootSystem.BaseChange, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{restrictScalarsRat}$ applied to $P$ is a root pairing of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{span} (\Rational , \operatorname{range} (\operatorname{coe} (\operatorname{root} (P))))}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (\Rational , \operatorname{range} (\operatorname{coe} (\operatorname{coroot} (P))))}{x_{7}})}$ defined as $\operatorname{restrictScalars}$ applied to $P$ and $\Rational$.
RootPairing.Base.mk'defMathlib.LinearAlgebra.RootSystem.BaseExists, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $s$ be an element of $\wp x$ such that $\mathrm{LinearIndepOn}$ holds for $R$, $\operatorname{coe}$ applied to the root of $P$ and $s$ and for all elements $i$ of $x$, $\operatorname{root}$ applied to $P$ and $i$ is an element of the closure of the image of $\operatorname{coe}$ applied to the root of $P$ and $s$ or $\operatorname{neg}$ applied to $\operatorname{root}$ applied to $P$ and $i$ is an element of the closure of the image of $\operatorname{coe}$ applied to the root of $P$ and $s$. Then $\operatorname{mk'}$ applied to $P$, $s$, $\mathrm{hli}$ and $\mathrm{hsp}$ is a base of $P$.
RootPairing.equiv_of_mapsTodefMathlib.LinearAlgebra.RootSystem.Basic, function or constantWording
the equivalence of coroot and i (from the name)
English
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $\mathrm{root}$ be an embedding of $x$ and $M$. Let $\mathrm{coroot}$ be an embedding of $x$ and $N$. Let $i$ be an element of $x$. Assume that for all elements $i_{2}$ of $x$, $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to the reflection of $\mathrm{root}$ applied to $i_{2}$ and $\operatorname{flip}$ applied to $p$ and $\mathrm{coroot}$ applied to $i_{2}$, the range of $\operatorname{coe}$ applied to $\mathrm{root}$ and the range of $\operatorname{coe}$ applied to $\mathrm{root}$. Assume that for all elements $i_{1}$ of $x$, $\EqtMACRoH {\operatorname{coe} (p , \mathrm{root} (i_{1}), \mathrm{coroot} (i_{1}))}{2}$. Then the equivalence of $\mathrm{coroot}$ and $i$ is an equivalence from $x$ to $x$.
RootPairing.mk'defMathlib.LinearAlgebra.RootSystem.Basic, function or constantEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $R$. Let $\mathrm{root}$ be an embedding of $x$ and $M$. Let $\mathrm{coroot}$ be an embedding of $x$ and $N$ such that for all elements $i_{2}$ of $x$, $\EqtMACRoH {\operatorname{coe} (p , \mathrm{root} (i_{2}), \mathrm{coroot} (i_{2}))}{2}$, for all elements $i_{1}$ of $x$, $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to the reflection of $\mathrm{root}$ applied to $i_{1}$ and $\operatorname{flip}$ applied to $p$ and $\mathrm{coroot}$ applied to $i_{1}$, the range of $\operatorname{coe}$ applied to $\mathrm{root}$ and the range of $\operatorname{coe}$ applied to $\mathrm{root}$ and for all elements $i$ of $x$, $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to the reflection of $\mathrm{coroot}$ applied to $i$ and $p$ applied to $\mathrm{root}$ applied to $i$, the range of $\operatorname{coe}$ applied to $\mathrm{coroot}$ and the range of $\operatorname{coe}$ applied to $\mathrm{coroot}$. Then $\operatorname{mk'}$ applied to $p$, $\mathrm{root}$, $\mathrm{coroot}$, $\mathrm{hp}$, $\mathrm{hr}$ and $\mathrm{hc}$ is a root pairing of $M$ and $N$.
RootPairing.mk''defMathlib.LinearAlgebra.RootSystem.Basic, function or constantEnglish
Let $p$ be a linear map of $M$ and the set of linear maps of $N$ and $k$. Let $\mathrm{root}$ be an embedding of $x$ and $M$. Let $\mathrm{coroot}$ be an embedding of $x$ and $N$ such that for all elements $i_{1}$ of $x$, $\EqtMACRoH {\operatorname{coe} (p , \mathrm{root} (i_{1}), \mathrm{coroot} (i_{1}))}{2}$ and for all elements $i$ of $x$, $\operatorname{MapsTo}$ holds for $\operatorname{coe}$ applied to the reflection of $\mathrm{root}$ applied to $i$ and $\operatorname{flip}$ applied to $p$ and $\mathrm{coroot}$ applied to $i$, the range of $\operatorname{coe}$ applied to $\mathrm{root}$ and the range of $\operatorname{coe}$ applied to $\mathrm{root}$. Assume that the span of $k$ and the range of $\operatorname{coe}$ applied to $\mathrm{root}$ is equal to the top. Then $\operatorname{mk''}$ applied to $p$, $\mathrm{root}$, $\mathrm{coroot}$, $\mathrm{hp}$, $\mathrm{hs}$ and $\mathrm{hsp}$ is a root pairing of $M$ and $N$.
RootPairing.Base.cartanMatrixdefMathlib.LinearAlgebra.RootSystem.CartanMatrix, function or constantWording
the Cartan matrix of b (from the docstring)
English
Let $b$ be a base of $P$. Then the Cartan matrix of $b$ is a matrix of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{7}})}$ and $\Integer$ defined as the Cartan matrix of $\Integer$ and $b$.
RootPairing.Base.cartanMatrixIndefMathlib.LinearAlgebra.RootSystem.CartanMatrix, function or constantWording
the Cartan matrix of S and b (from the docstring)
English
Let $S$ be a set. Let $b$ be a base of $P$. Then the Cartan matrix of $S$ and $b$ is a matrix of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$ and $S$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\operatorname{pairingIn}$ applied to $P$, $S$, $i_{1}$ and $j_{1}$.
RootPairing.Base.equivOfCartanMatrixEqdefMathlib.LinearAlgebra.RootSystem.CartanMatrix, function or constantWording
the equivalence of x14 and e (from the name)
English
Let $b$ be a base of $P$. Let $x_{14}$ be a base of $x_{13}$. Let $e$ be an element of $\EquivMACRoAE {(\SubtypeSet {x_{17}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{17}})})}{(\SubtypeSet {x_{18}}{(\MembershipmemMACRoT {\operatorname{support} (x_{14})}{x_{18}})})}$. Assume that for all elements $i$ of $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{16}})}$, for all elements $j$ of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{15}})}$, $\operatorname{cartanMatrix} (x_{14})= \operatorname{cartanMatrix} (b)$. Then the equivalence of $x_{14}$ and $e$ is an equivalence of $P$ and $x_{13}$.
RootPairing.chainBotCoeffdefMathlib.LinearAlgebra.RootSystem.Chain, function or constantWording
the chain bottom coefficient of i and j (from the name)
English
Let $i$ and $j$ be elements of $x$. Then the chain bottom coefficient of $i$ and $j$ is a natural number defined as $\mathrm{dite}$ applied to $\mathrm{LinearIndependent}$ applied to $R$ and $\operatorname{vecCons}$ applied to $\operatorname{root}$ applied to $P$ and $i$ and $\operatorname{vecCons}$ applied to $\operatorname{root}$ applied to $P$ and $j$ and $\operatorname{vecEmpty}$, the function that maps $h_{4}$ to $\operatorname{toNat}$ applied to $\operatorname{neg}$ applied to $\operatorname{choose}$ applied to $\mathrm{RootPairing\_\_setOfPred\_root\_add\_zsmul\_eq\_Icc\_of\_linearIndependent}$ applied to $h_{4}$ and the function that maps $h_{5}$ to $0$.
RootPairing.chainBotIdxdefMathlib.LinearAlgebra.RootSystem.Chain, function or constantWording
the chain bottom index of i and j (from the name)
English
Let $i$ and $j$ be elements of $x$. Then the chain bottom index of $i$ and $j$ is an element of $x$.
RootPairing.chainTopCoeffdefMathlib.LinearAlgebra.RootSystem.Chain, function or constantWording
the chain top coefficient of i and j (from the name)
English
Let $i$ and $j$ be elements of $x$. Then the chain top coefficient of $i$ and $j$ is a natural number.
RootPairing.chainTopIdxdefMathlib.LinearAlgebra.RootSystem.Chain, function or constantWording
the chain top index of i and j (from the name)
English
Let $i$ and $j$ be elements of $x$. Then the chain top index of $i$ and $j$ is an element of $x$.
RootDatumdefMathlib.LinearAlgebra.RootSystem.Defs, typeEnglish
Let $x$, $x_{1}$ and $x_{2}$ be sets. Then an element of $\mathrm{RootDatum}$ applied to $x$, $x_{1}$ and $x_{2}$ is an element of the function that maps $x$, $x_{1}$ and $x_{2}$ to the set of root pairings of $x_{1}$ and $x_{2}$.
RootPairingstructureMathlib.LinearAlgebra.RootSystem.Defs, typeWording
root pairing of M and N (from the name)
English
Let $x$, $R$, $M$ and $N$ be sets. Then the root pairings of $M$ and $N$ are a basic type.
RootPairing.IsOrthogonaldefMathlib.LinearAlgebra.RootSystem.Defs, predicateWording
i is orthogonal to j (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ and $j$ be elements of $x$. Then $i$ is orthogonal to $j$, if the pairing of $i$ and $j$ is equal to $0$ and the pairing of $j$ and $i$ is equal to $0$.
RootPairing.IsRootSystemclassMathlib.LinearAlgebra.RootSystem.Defs, predicateWording
P is a root system (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is a root system.
RootPairing.coreflectiondefMathlib.LinearAlgebra.RootSystem.Defs, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then $\operatorname{coreflection}$ applied to $P$ and $i$ is a linear equivalence of $N$ and $N$ defined as the reflection of $\mathrm{RootPairing\_\_root\_coroot\_two}$ applied to $P$ and $i$.
RootPairing.corootdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the coroot of self (from the name)
English
Let $\mathrm{self}$ be a root pairing of $M$ and $N$. Then the coroot of $\mathrm{self}$ is an embedding of $x$ and $N$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
RootPairing.coroot'defMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the coroot of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then the coroot of $P$ and $i$ is a dual of $R$ and $M$ defined as $\operatorname{flip}$ applied to $\operatorname{toLinearMap}$ applied to $P$ and $\operatorname{coroot}$ applied to $P$ and $i$.
RootPairing.coxeterWeightdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $i$ and $j$ be elements of $x$. Then $\operatorname{coxeterWeight}$ applied to $P$, $i$ and $j$ is an element of $R$ defined as the product of the pairing of $i$ and $j$ and the pairing of $j$ and $i$.
RootPairing.flipdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the flip of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the flip of $P$ is a root pairing of $N$ and $M$ defined as $\operatorname{mk}$ applied to the flip of $\operatorname{toLinearMap}$ applied to $P$, the coroot of $P$, the root of $P$, $\mathrm{RootPairing\_\_root\_coroot\_two}$ applied to $P$, $\operatorname{reflectionPerm}$ applied to $P$, $\mathrm{RootPairing\_\_reflectionPerm\_coroot}$ applied to $P$ and $\mathrm{RootPairing\_\_reflectionPerm\_root}$ applied to $P$.
RootPairing.flipEquivdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the flip equivalence of M and N (from the name)
English
Let $x$, $R$, $M$ and $N$ be sets. Then the flip equivalence of $M$ and $N$ is an equivalence from the set of root pairings of $N$ and $M$ to the set of root pairings of $M$ and $N$.
RootPairing.mapdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the map of f and g (from the name)
English
Let $e$ be an equivalence from $x$ to $x_{6}$. Let $f$ be a linear equivalence of $M$ and $x_{7}$. Let $g$ be a linear equivalence of $N$ and $x_{8}$. Then the map of $f$ and $g$ is a root pairing of $x_{7}$ and $x_{8}$.
RootPairing.pairingdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the pairing of i and j (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ and $j$ be elements of $x$. Then the pairing of $i$ and $j$ is an element of $R$ defined as $\operatorname{root'}$ applied to $P$, $i$ and $\operatorname{coroot}$ applied to $P$ and $j$.
RootPairing.reflectiondefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the reflection of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then the reflection of $P$ and $i$ is a linear equivalence of $M$ and $M$.
RootPairing.reflectionPermdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the reflection permutation of self and x6 (from the name)
English
Let $\mathrm{self}$ be a root pairing of $M$ and $N$. Let $x_{6}$ be an element of $x$. Then the reflection permutation of $\mathrm{self}$ and $x_{6}$ is an equivalence from $x$ to $x$ defined as $\operatorname{proj5}$ applied to $\mathrm{self}$ and $x_{6}$.
RootPairing.rootdefMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the root of self (from the name)
English
Let $\mathrm{self}$ be a root pairing of $M$ and $N$. Then the root of $\mathrm{self}$ is an embedding of $x$ and $M$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
RootPairing.root'defMathlib.LinearAlgebra.RootSystem.Defs, function or constantWording
the root of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then the root of $P$ and $i$ is a dual of $R$ and $N$ defined as $\operatorname{toLinearMap}$ applied to $P$ and $\operatorname{root}$ applied to $P$ and $i$.
RootPairing.CoPolarizationdefMathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{CoPolarization}$ applied to $P$ is a linear map of $N$ and $M$ defined as the polarization of the flip of $P$.
RootPairing.CoPolarizationIndefMathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then $\operatorname{CoPolarizationIn}$ applied to $P$ and $S$ is a linear map of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{corootSpan} (P , S)}{x_{11}})}$ and $M$ defined as $\operatorname{PolarizationIn}$ applied to the flip of $P$ and $S$.
RootPairing.PolarizationdefMathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear, function or constantWording
the polarization of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the polarization of $P$ is a linear map of $M$ and $N$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{toSpanSingleton} (\operatorname{coroot} (P , i)), \operatorname{coroot'} (P , i))}$.
RootPairing.PolarizationIndefMathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then $\operatorname{PolarizationIn}$ applied to $P$ and $S$ is a linear map of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{rootSpan} (P , S)}{x_{11}})}$ and $N$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{comp} (\operatorname{toSpanSingleton} (\operatorname{coroot} (P , i)), \operatorname{coroot'In} (P , S , i))}$.
RootPairing.RootFormIndefMathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then $\operatorname{RootFormIn}$ applied to $P$ and $S$ is a bilinear form of $S$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{rootSpan} (P , S)}{x_{10}})}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{smulRight} (\operatorname{coroot'In} (P , S , i), \operatorname{coroot'In} (P , S , i))}$.
RootPairing.EmbeddedG2classMathlib.LinearAlgebra.RootSystem.Finite.G2, predicateWording
P is embedded (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is embedded.
RootPairing.EmbeddedG2.allCoeffsdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
$\operatorname{allCoeffs}$ is a list of functions from elements of $\mathrm{Fin}$ applied to $2$ to integers defined as $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecCons}$ applied to $0$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $2$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $2$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $3$ and $\operatorname{vecCons}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $3$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $1$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $3$ and $\operatorname{vecCons}$ applied to $2$ and $\operatorname{vecEmpty}$ and $\operatorname{cons}$ applied to $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $3$ and $\operatorname{vecCons}$ applied to $\operatorname{neg}$ applied to $2$ and $\operatorname{vecEmpty}$ and $\operatorname{nil}$.
RootPairing.EmbeddedG2.allRootsdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the list of all roots of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the list of all roots of $P$ is a list of elements of $M$ defined as $\operatorname{cons}$ applied to the long root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the long root of $P$ and $\operatorname{cons}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to the short root of $P$ and $\operatorname{cons}$ applied to $\operatorname{neg}$ applied to the short root of $P$ and $\operatorname{nil}$.
RootPairing.EmbeddedG2.basisdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the basis of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the basis of $P$ is a basis of $R$ and $M$.
RootPairing.EmbeddedG2.indexEquivAllRootsdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{indexEquivAllRoots}$ applied to $P$ is an element of $\EquivMACRoAE {x}{(\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{toFinset} (\operatorname{allRoots} (P))}{x_{7}})})}$.
RootPairing.EmbeddedG2.longdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the distinguished long root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the distinguished long root of $P$ is an element of $x$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
RootPairing.EmbeddedG2.longRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the long root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the long root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and the distinguished long root of $P$.
RootPairing.EmbeddedG2.shortdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the distinguished short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the distinguished short root of $P$ is an element of $x$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.
RootPairing.EmbeddedG2.shortAddLongdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{shortAddLong}$ applied to $P$ is an element of $x$ defined as $\operatorname{reflectionPerm}$ applied to $P$, the distinguished long root of $P$ and the distinguished short root of $P$.
RootPairing.EmbeddedG2.shortAddLongRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the short root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and $\operatorname{shortAddLong}$ applied to $P$.
RootPairing.EmbeddedG2.shortRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the short root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and the distinguished short root of $P$.
RootPairing.EmbeddedG2.threeShortAddLongdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{threeShortAddLong}$ applied to $P$ is an element of $x$ defined as $\operatorname{reflectionPerm}$ applied to $P$, the distinguished short root of $P$ and the distinguished long root of $P$.
RootPairing.EmbeddedG2.threeShortAddLongRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the short root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and $\operatorname{threeShortAddLong}$ applied to $P$.
RootPairing.EmbeddedG2.threeShortAddTwoLongdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{threeShortAddTwoLong}$ applied to $P$ is an element of $x$ defined as $\operatorname{reflectionPerm}$ applied to $P$, the distinguished long root of $P$ and $\operatorname{reflectionPerm}$ applied to $P$, the distinguished short root of $P$ and the distinguished long root of $P$.
RootPairing.EmbeddedG2.threeShortAddTwoLongRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the short root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and $\operatorname{threeShortAddTwoLong}$ applied to $P$.
RootPairing.EmbeddedG2.twoShortAddLongdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{twoShortAddLong}$ applied to $P$ is an element of $x$ defined as $\operatorname{reflectionPerm}$ applied to $P$, the distinguished short root of $P$ and $\operatorname{reflectionPerm}$ applied to $P$, the distinguished long root of $P$ and the distinguished short root of $P$.
RootPairing.EmbeddedG2.twoShortAddLongRootdefMathlib.LinearAlgebra.RootSystem.Finite.G2, function or constantWording
the short root of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the short root of $P$ is an element of $M$ defined as $\operatorname{root}$ applied to $P$ and $\operatorname{twoShortAddLong}$ applied to $P$.
RootPairing.IsG2classMathlib.LinearAlgebra.RootSystem.Finite.G2, predicateEnglish
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $\operatorname{IsG2}$ holds for $P$.
RootPairing.IsNotG2classMathlib.LinearAlgebra.RootSystem.Finite.G2, predicateEnglish
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $\operatorname{IsNotG2}$ holds for $P$.
RootPairing.IsAnisotropicclassMathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate, predicateWording
P is anisotropic (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is anisotropic.
RootPairing.PolarizationEquivdefMathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate, function or constantWording
the polarization equivalence of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the polarization equivalence of $P$ is a linear equivalence of $M$ and $N$.
RootPairing.GeckConstruction.cartanSubalgebradefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantWording
the Cartan subalgebra of b (from the name)
English
Let $b$ be a base of $P$. Then the Cartan subalgebra of $b$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$ and $x$ and $R$.
RootPairing.GeckConstruction.cartanSubalgebra'defMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantWording
the Cartan subalgebra of b (from the name)
English
Let $b$ be a base of $P$. Then the Cartan subalgebra of $b$ is a Lie subalgebra of $R$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{lieAlgebra} (b)}{x_{8}})}$ defined as the preimage of the inclusion of the Lie algebra of $b$ and the Cartan subalgebra of $b$.
RootPairing.GeckConstruction.edefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $i$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$. Then there is a matrix of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{7}})}$ and $x$ and $R$. Proof. Let $i$ be arbitrary. By 0. Let $\mathrm{i'1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i'1. By i. By Eqt. By j1. By i. By Neg__neg. By Eqt. By and. By 1. By 0. By ite. By Matrix__of__app. Let $\mathrm{i'2}$ be arbitrary. Let $j_{2}$ be arbitrary. By i'2. By i. By Eqt. By b. By RootPairing__Base__cartanMatrix. By abs. By 0. By ite. By Matrix__of__app. Let $\mathrm{i'3}$ be arbitrary. Let $j_{3}$ be arbitrary. By P. By i'3. By RootPairing__root__app. By P. By i. By RootPairing__root__app. By P. By j3. By RootPairing__root__app. By plus. By Eqt. By i. By j3. By RootPairing__chainBotCoeff. By 1. By plus. By 0. By ite. By Matrix__of__app. By Matrix__fromBlocks.
RootPairing.GeckConstruction.fdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $i$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$. Then there is a matrix of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{7}})}$ and $x$ and $R$. Proof. Let $i$ be arbitrary. By 0. Let $\mathrm{i'1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i'1. By i. By Eqt. By j1. By i. By Eqt. By and. By 1. By 0. By ite. By Matrix__of__app. Let $\mathrm{i'2}$ be arbitrary. Let $j_{2}$ be arbitrary. By i'2. By i. By Neg__neg. By Eqt. By b. By RootPairing__Base__cartanMatrix. By abs. By 0. By ite. By Matrix__of__app. Let $\mathrm{i'3}$ be arbitrary. Let $j_{3}$ be arbitrary. By P. By i'3. By RootPairing__root__app. By P. By j3. By RootPairing__root__app. By P. By i. By RootPairing__root__app. By minus. By Eqt. By i. By j3. By RootPairing__chainTopCoeff. By 1. By plus. By 0. By ite. By Matrix__of__app. By Matrix__fromBlocks.
RootPairing.GeckConstruction.hdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $i$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$. Then there is a matrix of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{7}})}$ and $x$ and $R$. Proof. Let $i$ be arbitrary. By 0. By 0. By 0. Let $x_{6}$ be arbitrary. By P. By Int. By x6. By i. By RootPairing__pairingIn. By Matrix__diagonal. By Matrix__fromBlocks.
RootPairing.GeckConstruction.h'defMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $i$ be an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$. Then $\operatorname{h'}$ applied to $i$ is an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{cartanSubalgebra'} (b)}{x_{8}})}$ defined as $\operatorname{h}$ applied to $i$.
RootPairing.GeckConstruction.lieAlgebradefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantWording
the Lie algebra of b (from the name)
English
Let $b$ be a base of $P$. Then the Lie algebra of $b$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$ and $x$ and $R$ defined as the Lie span of $\UnionunionMACRoAB {(\UnionunionMACRoAB {\operatorname{range} (\operatorname{h})}{\operatorname{range} (\operatorname{e})})}{\operatorname{range} (\operatorname{f})}$.
RootPairing.GeckConstruction.udefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $i$ be an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$. Let $x_{7}$ be an element of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$ and $x$. Then $\operatorname{u}$ applied to $i$ and $x_{7}$ is an element of $R$ defined as $\operatorname{single}$ applied to $\operatorname{inl}$ applied to $i$, $1$ and $x_{7}$.
RootPairing.GeckConstruction.vdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $b$ be a base of $P$. Let $i$ be an element of $x$. Let $x_{7}$ be an element of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$ and $x$. Then $\operatorname{v}$ applied to $b$, $i$ and $x_{7}$ is an element of $R$ defined as $\operatorname{single}$ applied to $\operatorname{inr}$ applied to $i$, $1$ and $x_{7}$.
RootPairing.GeckConstruction.ωdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantEnglish
Let $b$ be a base of $P$. Then there is a matrix of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{7}})}$ and $x$ and $R$. Proof. Let $b$ be arbitrary. By 1. By 0. By 0. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By Neg__neg. By Eqt. By 1. By 0. By ite. By Matrix__of__app. By Matrix__fromBlocks.
RootPairing.GeckConstruction.ωConjdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantWording
the conjugation of b (from the docstring)
English
Let $b$ be a base of $P$. Then the conjugation of $b$ is a Lie equivalence of the set of matrixes of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{9}})}$ and $x$ and $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{11}})}$ and $x$ and $R$.
RootPairing.GeckConstruction.ωConjLieSubmoduledefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic, function or constantWording
the conjugate Lie submodule of N1 (from the name)
English
Let $N_{1}$ be a Lie submodule of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{lieAlgebra} (b)}{x_{11}})}$ and the set of functions from elements of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{13}})}$ and $x$ to elements of $R$. Then the conjugate Lie submodule of $N_{1}$ is a Lie submodule of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{lieAlgebra} (b)}{x_{8}})}$ and the set of functions from elements of $\mathrm{Sum}$ applied to $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{10}})}$ and $x$ to elements of $R$.
RootPairing.GeckConstruction.basisdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis, function or constantWording
the basis of b (from the name)
English
Let $b$ be a base of $P$. Then the basis of $b$ is a basis of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{support} (b)}{x_{8}})}$ and the Cartan subalgebra of $b$.
RootPairing.GeckConstruction.equivLieAlgebradefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis, function or constantWording
the equivalence Lie algebra of H and b (from the name)
English
Let $H$ be a Lie subalgebra of $K$ and $L$. Let $b$ be a base of the root system of $H$. Then the equivalence Lie algebra of $H$ and $b$ is a Lie equivalence of $L$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{lieAlgebra} (b)}{x_{3}})}$ defined as the equivalence of the equivalence root system of $b$.
RootPairing.GeckConstruction.equivRootSystemdefMathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis, function or constantWording
the equivalence root system of b (from the name)
English
Let $b$ be a base of $P$. Then the equivalence root system of $b$ is an equivalence of $P$ and the root system of the Cartan subalgebra of $b$.
RootPairing.AutdefMathlib.LinearAlgebra.RootSystem.Hom, typeWording
automorphism of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then an automorphism of $P$ is an element of the function that maps $P$ to the set of equivalences of $P$ and $P$.
RootPairing.EnddefMathlib.LinearAlgebra.RootSystem.Hom, typeWording
end of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then an end of $P$ is an element of the function that maps $P$ to the set of homomorphisms of $P$ and $P$.
RootPairing.EquivstructureMathlib.LinearAlgebra.RootSystem.Hom, typeWording
equivalence of P and Q (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $Q$ be a root pairing of $x_{7}$ and $x_{8}$. Then the equivalences of $P$ and $Q$ are a basic type.
RootPairing.Equiv.compdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be an equivalence of $x_{20}$ and $x_{21}$. Let $f$ be an equivalence of $P$ and $x_{20}$. Then the composition of $g$ and $f$ is an equivalence of $P$ and $x_{21}$.
RootPairing.Equiv.coweightEquivdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the coweight equivalence of e (from the name)
English
Let $e$ be an equivalence of $P$ and $Q$. Then the coweight equivalence of $e$ is a linear equivalence of $x_{8}$ and $N$ defined as the linear equivalence of the coweight map of $\operatorname{toHom}$ applied to $e$ and $\mathrm{RootPairing\_\_Equiv\_\_bijective\_coweightMap}$ applied to $e$.
RootPairing.Equiv.coweightHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the coweight homomorphism of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the coweight homomorphism of $P$ is a monoid homomorphism of the set of automorphisms of $P$ and the set of multiplicative opposites of the set of linear equivalences of $N$ and $N$.
RootPairing.Equiv.iddefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the identity equivalence of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the identity equivalence of $P$ is an equivalence of $P$ and $P$.
RootPairing.Equiv.indexHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the index homomorphism of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the index homomorphism of $P$ is a monoid homomorphism of the set of automorphisms of $P$ and $\EquivMACRoAE {x}{x}$.
RootPairing.Equiv.mk'defMathlib.LinearAlgebra.RootSystem.Hom, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $Q$ be a root pairing of $x_{7}$ and $x_{8}$. Let $f$ be a linear equivalence of $M$ and $x_{7}$. Let $e$ be an equivalence from $x$ to $x_{6}$ such that for all elements $i$ of $x$, $\EqtMACRoH {f (\operatorname{root} (P , i))}{\operatorname{root} (Q , e (i))}$. Then $\operatorname{mk'}$ applied to $P$, $Q$, $f$, $e$ and $\mathrm{hf}$ is an equivalence of $P$ and $Q$.
RootPairing.Equiv.reflectiondefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the automorphism of P and i (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then the automorphism of $P$ and $i$ is an automorphism of $P$.
RootPairing.Equiv.symmdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the inverse of Q and f (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $Q$ be a root pairing of $x_{7}$ and $x_{8}$. Let $f$ be an equivalence of $P$ and $Q$. Then the inverse of $Q$ and $f$ is an equivalence of $Q$ and $P$.
RootPairing.Equiv.toEndUnitdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the end unit of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the end unit of $P$ is a multiplicative equivalence of the set of automorphisms of $P$ and the set of units of the set of ends of $P$.
RootPairing.Equiv.weightEquivdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantEnglish
Let $e$ be an equivalence of $P$ and $Q$. Then $\operatorname{weightEquiv}$ applied to $e$ is a linear equivalence of $M$ and $x_{7}$ defined as the linear equivalence of $\operatorname{weightMap}$ applied to $\operatorname{toHom}$ applied to $e$ and $\mathrm{RootPairing\_\_Equiv\_\_bijective\_weightMap}$ applied to $e$.
RootPairing.Equiv.weightHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{weightHom}$ applied to $P$ is a monoid homomorphism of the set of automorphisms of $P$ and the set of linear equivalences of $M$ and $M$.
RootPairing.HomstructureMathlib.LinearAlgebra.RootSystem.Hom, typeWording
homomorphism of P and Q (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $Q$ be a root pairing of $x_{7}$ and $x_{8}$. Then the homomorphisms of $P$ and $Q$ are a basic type.
RootPairing.Hom.compdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the composition of g and f (from the name)
English
Let $g$ be a homomorphism of $x_{20}$ and $x_{21}$. Let $f$ be a homomorphism of $P$ and $x_{20}$. Then the composition of $g$ and $f$ is a homomorphism of $P$ and $x_{21}$.
RootPairing.Hom.coweightHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the coweight homomorphism of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the coweight homomorphism of $P$ is a monoid homomorphism of the set of ends of $P$ and the set of multiplicative opposites of the set of linear maps of $N$ and $N$.
RootPairing.Hom.coweightMapdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the coweight map of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $P$ and $Q$. Then the coweight map of $\mathrm{self}$ is a linear map of $x_{8}$ and $N$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.
RootPairing.Hom.iddefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the identity morphism of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the identity morphism of $P$ is a homomorphism of $P$ and $P$.
RootPairing.Hom.indexEquivdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the index equivalence of self (from the name)
English
Let $\mathrm{self}$ be a homomorphism of $P$ and $Q$. Then the index equivalence of $\mathrm{self}$ is an equivalence from $x$ to $x_{6}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.
RootPairing.Hom.indexHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantWording
the index homomorphism of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the index homomorphism of $P$ is a monoid homomorphism of the set of ends of $P$ and $\EquivMACRoAE {x}{x}$.
RootPairing.Hom.weightHomdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{weightHom}$ applied to $P$ is a monoid homomorphism of the set of ends of $P$ and the set of ends of $R$ and $M$.
RootPairing.Hom.weightMapdefMathlib.LinearAlgebra.RootSystem.Hom, function or constantEnglish
Let $\mathrm{self}$ be a homomorphism of $P$ and $Q$. Then $\operatorname{weightMap}$ applied to $\mathrm{self}$ is a linear map of $M$ and $x_{7}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.
RootPairing.IsIrreducibleclassMathlib.LinearAlgebra.RootSystem.Irreducible, predicateWording
P is irreducible (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is irreducible.
RootPairing.invtRootSubmoduledefMathlib.LinearAlgebra.RootSystem.Irreducible, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Then $\operatorname{invtRootSubmodule}$ applied to $P$ is a sublattice of the set of submodules of $R$ and $M$ defined as the infimum of the function that maps $i$ to $\operatorname{invtSubmodule}$ applied to $\operatorname{toLinearMap}$ applied to the reflection of $P$ and $i$.
RootPairing.IsCrystallographicdefMathlib.LinearAlgebra.RootSystem.IsValuedIn, predicateWording
P is crystallographic (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then $P$ is crystallographic, if $\operatorname{IsValuedIn}$ holds for $P$ and $\Integer$.
RootPairing.IsValuedInclassMathlib.LinearAlgebra.RootSystem.IsValuedIn, predicateEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then we can say that $\operatorname{IsValuedIn}$ holds for $P$ and $S$.
RootPairing.coroot'IndefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ be an element of $x$. Then $\operatorname{coroot'In}$ applied to $P$, $S$ and $i$ is a dual of $S$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{rootSpan} (P , S)}{x_{9}})}$ defined as $\operatorname{root'In}$ applied to the flip of $P$, $S$ and $i$.
RootPairing.corootSpandefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantWording
the coroot span of P and S (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then the coroot span of $P$ and $S$ is a submodule of $S$ and $N$ defined as the span of $S$ and the range of $\operatorname{coe}$ applied to the coroot of $P$.
RootPairing.corootSpanMemdefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantWording
the coroot span membership of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ be an element of $x$. Then the coroot span membership of $P$ and $i$ is an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{corootSpan} (P , S)}{x_{8}})}$ defined as $\operatorname{coroot}$ applied to $P$ and $i$.
RootPairing.coxeterWeightIndefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ and $j$ be elements of $x$. Then $\operatorname{coxeterWeightIn}$ applied to $P$, $S$, $i$ and $j$ is an element of $S$ defined as $\operatorname{pairingIn} (P , S , i , j)\times \operatorname{pairingIn} (P , S , j , i)$.
RootPairing.pairingIndefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ and $j$ be elements of $x$. Then $\operatorname{pairingIn}$ applied to $P$, $S$, $i$ and $j$ is an element of $S$ defined as $\operatorname{choose}$ applied to $\mathrm{RootPairing\_\_exists\_value}$ applied to $i$ and $j$.
RootPairing.root'IndefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantEnglish
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ be an element of $x$. Then $\operatorname{root'In}$ applied to $P$, $S$ and $i$ is a dual of $S$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{corootSpan} (P , S)}{x_{9}})}$.
RootPairing.rootSpandefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantWording
the root span of P and S (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Then the root span of $P$ and $S$ is a submodule of $S$ and $M$ defined as the span of $S$ and the range of $\operatorname{coe}$ applied to the root of $P$.
RootPairing.rootSpanMemdefMathlib.LinearAlgebra.RootSystem.IsValuedIn, function or constantWording
the root span membership of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $S$ be a set. Let $i$ be an element of $x$. Then the root span membership of $P$ and $i$ is an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{rootSpan} (P , S)}{x_{8}})}$ defined as $\operatorname{root}$ applied to $P$ and $i$.
LinearMap.IsReflectivestructureMathlib.LinearAlgebra.RootSystem.OfBilinear, predicateEnglish
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$. Let $x_{3}$ be an element of $M$. Then we can say that $\operatorname{IsReflective}$ holds for $B$ and $x_{3}$.
LinearMap.IsReflective.corootdefMathlib.LinearAlgebra.RootSystem.OfBilinear, function or constantWording
the coroot attached to a reflective vector of B and hx (from the docstring)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$ such that $\operatorname{IsReflective}$ holds for $B$ and $x_{3}$. Then the coroot attached to a reflective vector of $B$ and $\mathrm{hx}$ is a linear map of $M$ and $R$.
RootPairing.ofBilineardefMathlib.LinearAlgebra.RootSystem.OfBilinear, function or constantWording
the root pairing of B (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$ such that $B$ is non-degenerate and inverse. Assume that $2$ is a regular. Then the root pairing of $B$ is a root pairing of $M$ and the set of duals of $R$ and $M$.
RootPairing.IsReducedclassMathlib.LinearAlgebra.RootSystem.Reduced, predicateWording
P is reduced (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then we can say that $P$ is reduced.
RootPairingCatstructureMathlib.LinearAlgebra.RootSystem.RootPairingCat, typeWording
root pairing category of R (from the name)
English
Let $R$ be a set. Then the root pairing categories of $R$ are a basic type.
RootPairingCat.coweightdefMathlib.LinearAlgebra.RootSystem.RootPairingCat, typeWording
coweight of self (from the name)
English
Let $\mathrm{self}$ be a root pairing category of $R$. Then a coweight of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj3}$ applied to $\mathrm{self}$.
RootPairingCat.indexdefMathlib.LinearAlgebra.RootSystem.RootPairingCat, typeWording
index of self (from the name)
English
Let $\mathrm{self}$ be a root pairing category of $R$. Then an index of $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj6}$ applied to $\mathrm{self}$.
RootPairingCat.pairingdefMathlib.LinearAlgebra.RootSystem.RootPairingCat, function or constantWording
the root pairing structure of self (from the docstring)
English
Let $\mathrm{self}$ be a root pairing category of $R$. Then the root pairing structure of $\mathrm{self}$ is a root pairing of $\operatorname{weight}$ applied to $\mathrm{self}$ and the set of coweights of $\mathrm{self}$ defined as $\operatorname{proj7}$ applied to $\mathrm{self}$.
RootPairingCat.weightdefMathlib.LinearAlgebra.RootSystem.RootPairingCat, typeEnglish
Let $\mathrm{self}$ be a root pairing category of $R$. Then an element of $\operatorname{weight}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.
RootPairing.weylGroupdefMathlib.LinearAlgebra.RootSystem.WeylGroup, function or constantWording
the Weyl group of P (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Then the Weyl group of $P$ is a subgroup of the set of automorphisms of $P$ defined as the closure of the range of $\operatorname{reflection}$ applied to $P$.
RootPairing.weylGroup.ofIdxdefMathlib.LinearAlgebra.RootSystem.WeylGroup, function or constantWording
the Weyl group of P and i (from the name)
English
Let $P$ be a root pairing of $M$ and $N$. Let $i$ be an element of $x$. Then the Weyl group of $P$ and $i$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{weylGroup} (P)}{x_{6}})}$ defined as the automorphism of $P$ and $i$.
RootPairing.weylGroupCorootRepdefMathlib.LinearAlgebra.RootSystem.WeylGroup, function or constantWording
the natural representation of the Weyl group on the coroot space of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the natural representation of the Weyl group on the coroot space of $P$ is a representation of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{op} (\operatorname{weylGroup} (P))}{x_{6}})}$ and $N$ defined as the representation of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{op} (\operatorname{weylGroup} (P))}{x_{6}})}$ and $N$.
RootPairing.weylGroupRootRepdefMathlib.LinearAlgebra.RootSystem.WeylGroup, function or constantWording
the natural representation of the Weyl group on the root space of P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the natural representation of the Weyl group on the root space of $P$ is a representation of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{weylGroup} (P)}{x_{6}})}$ and $M$ defined as the representation of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{weylGroup} (P)}{x_{6}})}$ and $M$.
RootPairing.weylGroupToPermdefMathlib.LinearAlgebra.RootSystem.WeylGroup, function or constantWording
the permutation representation of the Weyl group induced by P (from the docstring)
English
Let $P$ be a root pairing of $M$ and $N$. Then the permutation representation of the Weyl group induced by $P$ is a monoid homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{weylGroup} (P)}{x_{6}})}$ and $\EquivMACRoAE {x}{x}$ defined as $\operatorname{domRestrict}$ applied to the index homomorphism of $P$ and the Weyl group of $P$.
SModEqdefMathlib.LinearAlgebra.SModEq.Basic, predicateEnglish
Let $U$ be a submodule of $R$ and $M$. Let $x_{3}$ and $y$ be elements of $M$. Then $\mathrm{SModEq}$ holds for $U$, $x_{3}$ and $y$, if $\EqtMACRoH {\operatorname{mk} (x_{3})}{\operatorname{mk} (y)}$.
Module.End.IsFinitelySemisimpledefMathlib.LinearAlgebra.Semisimple, predicateEnglish
Let $f$ be an end of $R$ and $M$. Then $\operatorname{IsFinitelySemisimple}$ holds for $f$, if for all submodules $p$ of $R$ and $M$, for all elements $\mathrm{hp}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {\operatorname{invtSubmodule} (f)}{p}$, if $\operatorname{Finite}$ holds for $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$, then $\operatorname{restrict}$ applied to $f$ and $\mathrm{hp}$ is semisimple.
Module.End.IsSemisimpledefMathlib.LinearAlgebra.Semisimple, predicateWording
f is semisimple (from the name)
English
Let $f$ be an end of $R$ and $M$. Then $f$ is semisimple, if $\mathrm{IsSemisimpleModule}$ holds for the set of polynomials of $R$ and the set of evaluations of $f$.
LinearMap.IsAdjointPairdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateEnglish
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $x_{1}$. Let $\mathrm{B'}$ be a linear map of $x$ and the set of linear maps of $x$ and $x_{1}$. Let $f$ be a function from elements of $M$ to elements of $x$. Let $g$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{IsAdjointPair}$ holds for $B$, $\mathrm{B'}$, $f$ and $g$, if for all elements $x_{9}$ of $M$, for all elements $y$ of $x$, $\EqtMACRoH {\operatorname{coe} (\mathrm{B'} , f (x_{9}), y)}{\operatorname{coe} (B , x_{9} , g (y))}$.
LinearMap.IsAltdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateEnglish
Let $B$ be a linear map of $x_{1}$ and the set of linear maps of $x_{1}$ and $M$. Then $\operatorname{IsAlt}$ holds for $B$, if for all elements $x_{10}$ of $x_{1}$, $\EqtMACRoH {\operatorname{coe} (B , x_{10} , x_{10})}{0}$.
LinearMap.IsNonnegstructureMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is nonnegative (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$. Then we can say that $B$ is nonnegative.
LinearMap.IsOrthogonaldefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
f is orthogonal to B (from the name)
English
Let $B$ be a bilinear form of $R$ and $M$. Let $f$ be a function from elements of $M$ to elements of $M$. Then $f$ is orthogonal to $B$, if for all elements $x_{3}$ and $y$ of $M$, $\EqtMACRoH {\operatorname{coe} (B , f (x_{3}), f (y))}{\operatorname{coe} (B , x_{3} , y)}$.
LinearMap.IsOrthoᵢdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateEnglish
Let $B$ be a linear map of $x_{1}$ and the set of linear maps of $x_{1}$ and $M$. Let $v$ be a function from elements of $n$ to elements of $x_{1}$. Then $\mathrm{LinearMap\_\_IsOrtho\_u1d62\_}$ holds for $B$ and $v$, if $\operatorname{onFun}$ applied to the function that maps $n_{1}$ and $m$ to $\EqtMACRoH {\operatorname{coe} (B , n_{1} , m)}{0}$ and $v$ is pairwise.
LinearMap.IsPairSelfAdjointdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateEnglish
Let $B$ and $F$ be linear maps of $M$ and the set of linear maps of $M$ and $x$. Let $f$ be a function from elements of $M$ to elements of $M$. Then $\operatorname{IsPairSelfAdjoint}$ holds for $B$, $F$ and $f$, if $\operatorname{IsAdjointPair}$ holds for $B$, $F$, $f$ and $f$.
LinearMap.IsPosSemidefstructureMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateEnglish
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$. Then we can say that $\operatorname{IsPosSemidef}$ holds for $B$.
LinearMap.IsRefldefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is a identity (from the name)
English
Let $B$ be a linear map of $x_{1}$ and the set of linear maps of $x_{1}$ and $M$. Then $B$ is an identity, if for all elements $x_{10}$ and $y$ of $x_{1}$, if $\EqtMACRoH {\operatorname{coe} (B , x_{10} , y)}{0}$, then $\EqtMACRoH {\operatorname{coe} (B , y , x_{10})}{0}$.
LinearMap.IsSelfAdjointdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is self-adjoint with respect to a bilinear map (from the docstring)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $x$. Let $f$ be a function from elements of $M$ to elements of $M$. Then $B$ is self-adjoint with respect to a bilinear map, if $\operatorname{IsAdjointPair}$ holds for $B$, $B$, $f$ and $f$.
LinearMap.IsSkewAdjointdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
f is a skew adjoint with respect to B (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $x$. Let $f$ be a function from elements of $M$ to elements of $M$. Then $f$ is a skew adjoint with respect to $B$, if $\operatorname{IsAdjointPair}$ holds for $B$, $B$, $f$ and $\operatorname{neg}$ applied to $f$.
LinearMap.IsSymmstructureMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is inverse (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $R$. Then we can say that $B$ is inverse.
LinearMap.NondegeneratedefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is non-degenerate (from the docstring)
English
Let $B$ be a linear map of $x_{2}$ and the set of linear maps of $x_{3}$ and $M$. Then $B$ is non-degenerate, if $B$ is a left separating and $B$ is a right separating.
LinearMap.SeparatingLeftdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is a left separating (from the name)
English
Let $B$ be a linear map of $x_{2}$ and the set of linear maps of $x_{3}$ and $M$. Then $B$ is a left separating, if for all elements $x_{15}$ of $x_{2}$, if for all elements $y$ of $x_{3}$, $\EqtMACRoH {\operatorname{coe} (B , x_{15} , y)}{0}$, then $\EqtMACRoH {x_{15}}{0}$.
LinearMap.SeparatingRightdefMathlib.LinearAlgebra.SesquilinearForm.Basic, predicateWording
B is a right separating (from the name)
English
Let $B$ be a linear map of $x_{2}$ and the set of linear maps of $x_{3}$ and $M$. Then $B$ is a right separating, if for all elements $y$ of $x_{3}$, if for all elements $x_{15}$ of $x_{2}$, $\EqtMACRoH {\operatorname{coe} (B , x_{15} , y)}{0}$, then $\EqtMACRoH {y}{0}$.
LinearMap.isPairSelfAdjointSubmoduledefMathlib.LinearAlgebra.SesquilinearForm.Basic, function or constantEnglish
Let $B$ and $F$ be linear maps of $M$ and the set of linear maps of $M$ and $x$. Then $\operatorname{isPairSelfAdjointSubmodule}$ applied to $B$ and $F$ is a submodule of $R$ and the set of ends of $R$ and $M$.
LinearMap.selfAdjointSubmoduledefMathlib.LinearAlgebra.SesquilinearForm.Basic, function or constantWording
the self adjoint submodule of B (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $x$. Then the self adjoint submodule of $B$ is a submodule of $R$ and the set of ends of $R$ and $M$ defined as $\operatorname{isPairSelfAdjointSubmodule}$ applied to $B$ and $B$.
LinearMap.skewAdjointSubmoduledefMathlib.LinearAlgebra.SesquilinearForm.Basic, function or constantWording
the skew adjoint submodule of B (from the name)
English
Let $B$ be a linear map of $M$ and the set of linear maps of $M$ and $x$. Then the skew adjoint submodule of $B$ is a submodule of $R$ and the set of ends of $R$ and $M$ defined as $\operatorname{isPairSelfAdjointSubmodule}$ applied to $\operatorname{neg}$ applied to $B$ and $B$.
Submodule.orthogonalBilindefMathlib.LinearAlgebra.SesquilinearForm.Orthogonal, function or constantWording
the orthogonal complement of B and S (from the docstring)
English
Let $B$ be a linear map of $x_{2}$ and the set of linear maps of $x_{3}$ and $M$. Let $S$ be a submodule of $x$ and $x_{2}$. Then the orthogonal complement of $B$ and $S$ is a submodule of $x_{1}$ and $x_{3}$.
LinearEquiv.coorddefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the coordinate of x3 (from the name)
English
Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $M$ such that $x_{3} \neq 0$. Then the coordinate of $x_{3}$ is a linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$ and $R$ defined as the inverse of the span nonzero singleton of $x_{3}$.
LinearEquiv.toSpanNonzeroSingletondefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the span nonzero singleton of x3 (from the name)
English
Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $M$ such that $x_{3} \neq 0$. Then the span nonzero singleton of $x_{3}$ is a linear equivalence of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$.
LinearMap.toSpanSingletondefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the span singleton of x3 (from the name)
English
Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $M$. Then the span singleton of $x_{3}$ is a linear map of $R$ and $M$ defined as the right scalar multiple of the identity and $x_{3}$.
Submodule.inclusionSpandefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the inclusion of S and p (from the docstring)
English
Let $S$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the inclusion of $S$ and $p$ is a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (S , p)}{x_{7}})}$.
Submodule.proddefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the product of p and x5 (from the name)
English
Let $p$ be a submodule of $R$ and $M$. Let $x_{5}$ be a submodule of $R$ and $\mathrm{M'}$. Then the product of $p$ and $x_{5}$ is a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$.
Submodule.prodEquivdefMathlib.LinearAlgebra.Span.Basic, function or constantWording
the product submodule of p and q (from the docstring)
English
Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $R$ and $\mathrm{M'}$. Then the product submodule of $p$ and $q$ is a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{prod} (p , q)}{x_{5}})}$ and $\mathrm{Prod}$ applied to $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {q}{x_{7}})}$.
Module.IsPrincipaldefMathlib.LinearAlgebra.Span.Defs, predicateWording
R is principal (from the docstring)
English
Let $R$ and $M$ be sets. Then $R$ is principal, if the top is principal.
Submodule.IsPrincipalclassMathlib.LinearAlgebra.Span.Defs, predicateWording
S is principal (from the name)
English
Let $S$ be a submodule of $R$ and $M$. Then we can say that $S$ is principal.
Submodule.IsPrincipal.generatordefMathlib.LinearAlgebra.Span.Defs, function or constantWording
the generator of S (from the name)
English
Let $S$ be a submodule of $R$ and $M$. Then the generator of $S$ is an element of $M$ defined as $\operatorname{choose}$ applied to $\operatorname{principal}$ applied to $S$.
Submodule.gidefMathlib.LinearAlgebra.Span.Defs, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{gi}$ applied to $R$ and $M$ is a Galois insertion of $\operatorname{span}$ applied to $R$ and $\operatorname{setLike}$.
Submodule.spandefMathlib.LinearAlgebra.Span.Defs, function or constantWording
the span of R and s (from the docstring)
English
Let $R$ be a set. Let $s$ be an element of $\wp M$. Then the span of $R$ and $s$ is a submodule of $R$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $p$ to $\mathrm{Leq} (s , p)$.
Submodule.tensorEquivSpandefMathlib.LinearAlgebra.Span.TensorProduct, function or constantWording
the tensor equivalence span of A and p (from the name)
English
Let $A$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the tensor equivalence span of $A$ and $p$ is a linear equivalence of the set of tensor products of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (A , p)}{x_{7}})}$.
Submodule.tensorSpanEquivSpandefMathlib.LinearAlgebra.Span.TensorProduct, function or constantWording
the tensor span equivalence span of s (from the name)
English
Let $R$ and $A$ be sets. Let $s$ be an element of $\wp M$. Then the tensor span equivalence span of $s$ is a linear equivalence of the set of tensor products of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{span} (R , s)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (A , s)}{x_{7}})}$.
Submodule.tensorToSpandefMathlib.LinearAlgebra.Span.TensorProduct, function or constantWording
the tensor to span of A and p (from the name)
English
Let $A$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the tensor to span of $A$ and $p$ is a linear map of the set of tensor products of $A$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (A , p)}{x_{7}})}$.
Matrix.SpecialLinearGroup.toLin'_equivdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the linear equivalence (from the name)
English
The linear equivalence is a multiplicative equivalence of the set of special linear groups of $n$ and $R$ and the set of special linear groups of $R$ and the set of functions from elements of $n$ to elements of $R$.
Matrix.SpecialLinearGroup.toLin_equivdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the linear equivalence of b (from the name)
English
Let $b$ be a basis of $R$ and $V$. Then the linear equivalence of $b$ is a multiplicative equivalence of the set of special linear groups of $n$ and $R$ and the set of special linear groups of $R$ and $V$ defined as the composition of the linear equivalence and the congruence linear equivalence of the inverse of the equivalence function of $b$.
SpecialLinearGroupdefMathlib.LinearAlgebra.SpecialLinearGroup, typeWording
special linear group of R and V (from the name)
English
Let $R$ and $V$ be sets. Then a special linear group of $R$ and $V$ is an element of the function that maps $R$ and $V$ to $\SubtypeSet {u}{(\EqtMACRoH {\operatorname{det} (u)}{1})}$.
SpecialLinearGroup.baseChangedefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the base change (from the name)
English
The base change is a monoid homomorphism of the set of special linear groups of $R$ and $V$ and the set of special linear groups of $S$ and the set of tensor products of $S$ and $V$.
SpecialLinearGroup.centerEquivRootsOfUnitydefMathlib.LinearAlgebra.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} (\mathrm{SpecialLinearGroup} (R , V))}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\MaxmaxMACRoAF {\operatorname{finrank} (R , V)}{1}, R)}{x_{4}})}$.
SpecialLinearGroup.centerEquivRootsOfUnity_invFundefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the inverse map for the equivalence of r (from the docstring)
English
Let $r$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{rootsOfUnity} (\MaxmaxMACRoAF {\operatorname{finrank} (R , V)}{1}, R)}{x_{4}})}$. Then the inverse map for the equivalence of $r$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{center} (\mathrm{SpecialLinearGroup} (R , V))}{x_{3}})}$.
SpecialLinearGroup.congr_linearEquivdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the congruence linear equivalence of e (from the name)
English
Let $e$ be a linear equivalence of $V$ and $W$. Then the congruence linear equivalence of $e$ is a multiplicative equivalence of the set of special linear groups of $R$ and $V$ and the set of special linear groups of $R$ and $W$.
SpecialLinearGroup.dualMapdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the dual map of A (from the name)
English
Let $A$ be a special linear group of $R$ and $V$. Then the dual map of $A$ is a special linear group of $R$ and the set of duals of $R$ and $V$ defined as the dual map of $A$.
SpecialLinearGroup.toGeneralLinearGroupdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the general linear group (from the name)
English
The general linear group is a monoid homomorphism of the set of special linear groups of $R$ and $V$ and the set of general linear groups of $R$ and $V$ defined as the composition of the monoid homomorphism of the inverse of the general linear group on $R$ and $V$ and the linear equivalence.
SpecialLinearGroup.toLinearEquivdefMathlib.LinearAlgebra.SpecialLinearGroup, function or constantWording
the linear equivalence (from the name)
English
The linear equivalence is a monoid homomorphism of the set of special linear groups of $R$ and $V$ and the set of linear equivalences of $V$ and $V$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to $A$ and $\mathrm{SpecialLinearGroup\_\_coe\_one}$ and $\mathrm{SpecialLinearGroup\_\_coe\_mul}$.
Module.piEquivdefMathlib.LinearAlgebra.StdBasis, function or constantWording
the product equivalence of R and M (from the name)
English
Let $x$, $R$ and $M$ be sets. Then the product equivalence of $R$ and $M$ is a linear equivalence of the set of functions from elements of $x$ to elements of $M$ and the set of linear maps of the set of functions from elements of $x$ to elements of $R$ and $M$ defined as $\operatorname{constr}$ applied to the basis function of $R$ and $x$ and $R$.
Pi.basisdefMathlib.LinearAlgebra.StdBasis, function or constantWording
the basis of s (from the name)
English
Let $s$ be a function from elements $j_{2}$ of $x$ to bases of $R$ and $\mathrm{Ms}$ applied to $j_{2}$. Then the basis of $j_{2}$ is a basis of $R$ and the set of functions from elements $j_{1}$ of $x$ to elements of $\mathrm{Ms}$ applied to $j_{1}$ defined as the function that maps $s$ to $\operatorname{ofRepr}$ applied to the composition of the right product congruence of the function that maps $j$ to the representation of $j_{2}$ applied to $j$ and the inverse of the sigma finitely supported function equivalence product finitely supported function of $R$ and $s$.
Pi.basisFundefMathlib.LinearAlgebra.StdBasis, function or constantWording
the basis function of R and x (from the name)
English
Let $R$ and $x$ be sets. Then the basis function of $R$ and $x$ is a basis of $R$ and the set of functions from elements of $x$ to elements of $R$ defined as the basis of the identity map of $R$ and the set of functions from elements of $x$ to elements of $R$.
Pi.spanSubsetdefMathlib.LinearAlgebra.StdBasis, function or constantWording
the span subset of R and s (from the name)
English
Let $R$ be a set. Let $s$ be an element of $\wp x$. Then the span subset of $R$ and $s$ is a submodule of $R$ and the set of functions from elements of $x$ to elements of $R$ defined as the span of $R$ and the image of $\operatorname{coe}$ applied to the basis function of $R$ and $x$ and $s$.
IsSymmetricAlgebradefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, predicateWording
f is a symmetric algebra (from the name)
English
Let $f$ be a linear map of $M$ and $A$. Then $f$ is a symmetric algebra, if $\operatorname{coe}$ applied to $\operatorname{lift}$ applied to $f$ is bijective.
IsSymmetricAlgebra.equivdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the equivalence of h (from the name)
English
Assume that $f$ is a symmetric algebra. Then the equivalence of $h$ is an algebra isomorphism of the set of symmetric algebras of $R$ and $M$ and $A$ defined as the algebra isomorphism of $\operatorname{lift}$ applied to $f$ and $h$.
IsSymmetricAlgebra.liftdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the lift of h and g (from the name)
English
Assume that $f$ is a symmetric algebra. Let $g$ be a linear map of $M$ and $\mathrm{A'}$. Then the lift of $h$ and $g$ is an algebra homomorphism of $A$ and $\mathrm{A'}$ defined as the composition of $\operatorname{lift}$ applied to $g$ and the algebra homomorphism of the inverse of the equivalence of $h$.
SymmetricAlgebradefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, typeWording
symmetric algebra of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a symmetric algebra of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of quotients of the symmetric power ring congruence relation of $R$ and $M$.
SymmetricAlgebra.algHomdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the algebra homomorphism of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the algebra homomorphism of $R$ and $M$ is an algebra homomorphism of the set of tensor algebras of $R$ and $M$ and the set of symmetric algebras of $R$ and $M$ defined as $\mathrm{RingCon\_\_mk\_u2090\_}$ applied to $R$ and the symmetric power ring congruence relation of $R$ and $M$.
SymmetricAlgebra.algebraMapInvdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the algebra map inverse (from the name)
English
The algebra map inverse is an algebra homomorphism of the set of symmetric algebras of $R$ and $M$ and $R$ defined as $\operatorname{lift}$ applied to $0$.
SymmetricAlgebra.liftdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the lift (from the name)
English
The lift is an equivalence from the set of linear maps of $M$ and $A$ to the set of algebra homomorphisms of the set of symmetric algebras of $R$ and $M$ and $A$.
SymmetricAlgebra.ιdefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the inclusion of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the inclusion of $R$ and $M$ is a linear map of $M$ and the set of symmetric algebras of $R$ and $M$ defined as the composition of the linear map of the algebra homomorphism of $R$ and $M$ and the inclusion of $R$.
TensorAlgebra.SymRelinductiveMathlib.LinearAlgebra.SymmetricAlgebra.Basic, predicateEnglish
Let $R$ and $M$ be sets. Let $x_{3}$ and $x_{4}$ be tensor algebras of $R$ and $M$. Then we can say that $\operatorname{SymRel}$ holds for $R$, $M$, $x_{3}$ and $x_{4}$.
TensorAlgebra.symRingCondefMathlib.LinearAlgebra.SymmetricAlgebra.Basic, function or constantWording
the symmetric power ring congruence relation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the symmetric power ring congruence relation of $R$ and $M$ is a ring congruence relation of the set of tensor algebras of $R$ and $M$ defined as the ring congruence relation generator of $\operatorname{SymRel}$ applied to $R$ and $M$.
Module.Basis.symmetricAlgebradefMathlib.LinearAlgebra.SymmetricAlgebra.Basis, function or constantWording
the symmetric algebra of b (from the name)
English
Let $b$ be a basis of $R$ and $M$. Then the symmetric algebra of $b$ is a basis of $R$ and the set of symmetric algebras of $R$ and $M$ defined as the map of the basis monomial of $x$ and $R$ and the linear equivalence of the inverse of the equivalence multivariate polynomial of $b$.
SymmetricAlgebra.equivMvPolynomialdefMathlib.LinearAlgebra.SymmetricAlgebra.Basis, function or constantWording
the equivalence multivariate polynomial of b (from the name)
English
Let $b$ be a basis of $R$ and $M$. Then the equivalence multivariate polynomial of $b$ is an algebra isomorphism of the set of symmetric algebras of $R$ and $M$ and the set of multivariate polynomials of $x$ and $R$.
Matrix.JdefMathlib.LinearAlgebra.SymplecticGroup, function or constantEnglish
Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By 0. By 1. By Neg__neg. By 1. By 0. By Matrix__fromBlocks.
Matrix.symplecticGroupdefMathlib.LinearAlgebra.SymplecticGroup, function or constantWording
the symplectic group of l and R (from the name)
English
Let $l$ and $R$ be sets. Then the symplectic group of $l$ and $R$ is a submonoid of the set of matrixes of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$.
SymplecticGroup.symJdefMathlib.LinearAlgebra.SymplecticGroup, function or constantWording
the symmetric power of l and R (from the name)
English
Let $l$ and $R$ be sets. Then the symmetric power of $l$ and $R$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{symplecticGroup} (l , R)}{x_{3}})}$ defined as $\operatorname{J}$ applied to $l$ and $R$.
FreeAlgebra.toTensordefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the tensor (from the name)
English
The tensor is an algebra homomorphism of the set of free algebras of $R$ and $M$ and the set of tensor algebras of $R$ and $M$ defined as $\operatorname{lift}$ applied to $R$ and $\operatorname{coe}$ applied to the inclusion of $R$.
TensorAlgebradefMathlib.LinearAlgebra.TensorAlgebra.Basic, typeWording
tensor algebra of R and M (from the name)
English
Let $R$ and $M$ be sets. Then a tensor algebra of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of quotients of the ring congruence relation of $R$ and $M$.
TensorAlgebra.RelinductiveMathlib.LinearAlgebra.TensorAlgebra.Basic, predicateEnglish
Let $R$ and $M$ be sets. Let $x_{3}$ and $x_{4}$ be free algebras of $R$ and $M$. Then we can say that $\operatorname{Rel}$ holds for $R$, $M$, $x_{3}$ and $x_{4}$.
TensorAlgebra.algebraMapInvdefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the algebra map inverse (from the name)
English
The algebra map inverse is an algebra homomorphism of the set of tensor algebras of $R$ and $M$ and $R$ defined as $\operatorname{lift}$ applied to $R$ and $0$.
TensorAlgebra.liftdefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the lift of R (from the name)
English
Let $R$ be a set. Then the lift of $R$ is an equivalence from the set of linear maps of $M$ and $A$ to the set of algebra homomorphisms of the set of tensor algebras of $R$ and $M$ and $A$.
TensorAlgebra.ringCondefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the ring congruence relation of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the ring congruence relation of $R$ and $M$ is a ring congruence relation of the set of free algebras of $R$ and $M$ defined as the ring congruence relation generator of $\operatorname{Rel}$ applied to $R$ and $M$.
TensorAlgebra.toTrivSqZeroExtdefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the trivial square zero extension (from the name)
English
The trivial square zero extension is an algebra homomorphism of the set of tensor algebras of $R$ and $M$ and the set of trivial square zero extensions of $R$ and $M$ defined as $\operatorname{lift}$ applied to $R$ and the right injection homomorphism of $R$ and $M$.
TensorAlgebra.tproddefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantEnglish
Let $R$ and $M$ be sets. Let $n$ be a natural number. Then $\operatorname{tprod}$ applied to $R$, $M$ and $n$ is a multilinear map of the function that maps $x_{3}$ to $M$ and the set of tensor algebras of $R$ and $M$ defined as the composition linear map of $\operatorname{mkPiAlgebraFin}$ applied to $R$, $n$ and the set of tensor algebras of $R$ and $M$ and the function that maps $x_{3}$ to the inclusion of $R$.
TensorAlgebra.ιdefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the inclusion of R (from the name)
English
Let $R$ be a set. Then the inclusion of $R$ is a linear map of $M$ and the set of tensor algebras of $R$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{TensorAlgebra\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_TensorAlgebra\_\_Basic\_\_1559328716\_\_\_hygCtx\_\_\_hyg\_\_8}$ and $R$.
TensorAlgebra.ιInvdefMathlib.LinearAlgebra.TensorAlgebra.Basic, function or constantWording
the inclusion inverse (from the name)
English
The inclusion inverse is a linear map of the set of tensor algebras of $R$ and $M$ and $M$ defined as the composition of the second component homomorphism of $R$ and $M$ and the linear map of the trivial square zero extension.
Module.Basis.tensorAlgebradefMathlib.LinearAlgebra.TensorAlgebra.Basis, function or constantWording
the tensor algebra of b (from the name)
English
Let $b$ be a basis of $R$ and $M$. Then the tensor algebra of $b$ is a basis of $R$ and the set of tensor algebras of $R$ and $M$ defined as the map of the basis free monoid of $R$ and $x$ and the linear equivalence of the inverse of the equivalence free algebra of $b$.
TensorAlgebra.equivFreeAlgebradefMathlib.LinearAlgebra.TensorAlgebra.Basis, function or constantWording
the equivalence free algebra of b (from the name)
English
Let $b$ be a basis of $R$ and $M$. Then the equivalence free algebra of $b$ is an algebra isomorphism of the set of tensor algebras of $R$ and $M$ and the set of free algebras of $R$ and $x$.
TensorAlgebra.GradedAlgebra.ιdefMathlib.LinearAlgebra.TensorAlgebra.Grading, function or constantWording
the inclusion of R and M (from the name)
English
Let $R$ and $M$ be sets. Then the inclusion of $R$ and $M$ is a linear map of $M$ and the set of direct sums of $\Natural$ and the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {(\operatorname{range} (\mathrm{TensorAlgebra\_\_\_u3b9\_} (R))^ {i})}{x_{3}})}$.
TensorAlgebra.equivDirectSumdefMathlib.LinearAlgebra.TensorAlgebra.ToTensorPower, function or constantWording
the equivalence direct sum (from the name)
English
The equivalence direct sum is an algebra isomorphism of the set of tensor algebras of $R$ and $M$ and the set of direct sums of $\Natural$ and the function that maps $n$ to the set of tensor powers of $n$ and $M$ defined as the algebra isomorphism of the canonical map from the tensor algebra to a direct sum of tensor powers and the canonical map.
TensorAlgebra.ofDirectSumdefMathlib.LinearAlgebra.TensorAlgebra.ToTensorPower, function or constantWording
the canonical map (from the docstring)
English
The canonical map is an algebra homomorphism of the set of direct sums of $\Natural$ and the function that maps $n$ to the set of tensor powers of $n$ and $M$ and the set of tensor algebras of $R$ and $M$ defined as the algebra of the function that maps $n$ to the set of tensor powers of $n$ and $M$ and the function that maps $x_{3}$ to the canonical embedding.
TensorAlgebra.toDirectSumdefMathlib.LinearAlgebra.TensorAlgebra.ToTensorPower, function or constantWording
the canonical map from the tensor algebra to a direct sum of tensor powers (from the docstring)
English
The canonical map from the tensor algebra to a direct sum of tensor powers is an algebra homomorphism of the set of tensor algebras of $R$ and $M$ and the set of direct sums of $\Natural$ and the function that maps $n$ to the set of tensor powers of $n$ and $M$ defined as $\operatorname{lift}$ applied to $R$ and the composition of $\operatorname{lof}$ applied to $R$, $\Natural$, the function that maps $n_{2}$ to the set of tensor powers of $n_{2}$ and $M$ and $1$ and $\operatorname{toLinearMap}$ applied to the inverse of the subsingleton equivalence of $0$.
TensorPower.toTensorAlgebradefMathlib.LinearAlgebra.TensorAlgebra.ToTensorPower, function or constantWording
the canonical embedding (from the docstring)
English
The canonical embedding is a linear map of the set of tensor powers of $n$ and $M$ and the set of tensor algebras of $R$ and $M$ defined as $\operatorname{lift}$ applied to $\operatorname{tprod}$ applied to $R$, $M$ and $n$.
TensorPowerdefMathlib.LinearAlgebra.TensorPower.Basic, typeWording
tensor power of n and M (from the name)
English
Let $R$ and $M$ be sets. Let $n$ be a natural number. Then a tensor power of $n$ and $M$ is an element of the function that maps $R$, $n$ and $M$ to the set of product tensor products of $R$ and the function that maps $x_{3}$ to $M$.
TensorPower.algebraMap₀defMathlib.LinearAlgebra.TensorPower.Basic, function or constantWording
the algebra map (from the name)
English
The algebra map is a linear equivalence of $R$ and the set of tensor powers of $0$ and $M$ defined as the inverse of the tensor product of $\mathrm{Fin}$ applied to $0$.
TensorPower.castdefMathlib.LinearAlgebra.TensorPower.Basic, function or constantWording
the cast of M and h (from the name)
English
Let $R$ and $M$ be sets. Assume that $i = j$. Then the cast of $M$ and $h$ is a linear equivalence of the set of tensor powers of $i$ and $M$ and the set of tensor powers of $j$ and $M$ defined as the reindexing of the function that maps $x_{3}$ to $M$ and the finite congruence of $h$.
TensorPower.mulEquivdefMathlib.LinearAlgebra.TensorPower.Basic, function or constantWording
the multiplicative equivalence (from the name)
English
The multiplicative equivalence is a linear equivalence of the set of tensor products of the set of tensor powers of $n$ and $M$ and the set of tensor powers of $m$ and $M$ and the set of tensor powers of $n + m$ and $M$ defined as the composition of $\operatorname{tmulEquiv}$ applied to $R$ and $M$ and the reindexing of the function that maps $x_{3}$ to $M$ and the finite sum finite equivalence.
TensorPower.multilinearMapToDualdefMathlib.LinearAlgebra.TensorPower.Pairing, function or constantWording
the multilinear map to dual of n (from the name)
English
Let $R$ and $M$ be sets. Let $n$ be a natural number. Then the multilinear map to dual of $n$ is a multilinear map of the function that maps $x_{3}$ to the set of duals of $R$ and $M$ and the set of duals of $R$ and the set of tensor powers of $n$ and $M$.
TensorPower.pairingDualdefMathlib.LinearAlgebra.TensorPower.Pairing, function or constantWording
the pairing dual of n (from the name)
English
Let $R$ and $M$ be sets. Let $n$ be a natural number. Then the pairing dual of $n$ is a linear map of the set of tensor powers of $n$ and the set of duals of $R$ and $M$ and the set of duals of $R$ and the set of tensor powers of $n$ and $M$ defined as $\operatorname{lift}$ applied to the multilinear map to dual of $n$.
SymmetricPowerdefMathlib.LinearAlgebra.TensorPower.Symmetric, typeWording
symmetric power of x and M (from the name)
English
Let $R$, $x$ and $M$ be sets. Then a symmetric power of $x$ and $M$ is an element of the function that maps $R$, $x$ and $M$ to the set of quotients of the additive congruence relation generator of $\operatorname{Rel}$ applied to $R$, $x$ and $M$.
SymmetricPower.RelinductiveMathlib.LinearAlgebra.TensorPower.Symmetric, predicateEnglish
Let $R$, $x$ and $M$ be sets. Let $x_{4}$ be a product tensor product of $R$ and the function that maps $x_{7}$ to $M$. Let $x_{5}$ be a product tensor product of $R$ and the function that maps $x_{6}$ to $M$. Then we can say that $\operatorname{Rel}$ holds for $R$, $x$, $M$, $x_{4}$ and $x_{5}$.
SymmetricPower.mkdefMathlib.LinearAlgebra.TensorPower.Symmetric, function or constantEnglish
Let $R$, $x$ and $M$ be sets. Then $\operatorname{mk}$ applied to $R$, $x$ and $M$ is a linear map of the set of product tensor products of $R$ and the function that maps $x_{4}$ to $M$ and the set of symmetric powers of $x$ and $M$.
SymmetricPower.smul'defMathlib.LinearAlgebra.TensorPower.Symmetric, function or constantWording
the scalar multiple of r (from the name)
English
Let $x$ and $M$ be sets. Let $r$ be an element of $R$. Then the scalar multiple of $r$ is an additive monoid homomorphism of the set of symmetric powers of $x$ and $M$ and the set of symmetric powers of $x$ and $M$.
SymmetricPower.tproddefMathlib.LinearAlgebra.TensorPower.Symmetric, function or constantEnglish
Let $R$ be a set. Then $\operatorname{tprod}$ applied to $R$ is a multilinear map of the function that maps $x_{4}$ to $M$ and the set of symmetric powers of $x$ and $M$ defined as the composition multilinear map of $\operatorname{mk}$ applied to $R$, $x$ and $M$ and $\operatorname{tprod}$ applied to $R$.
TensorProduct.assocdefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantWording
the associator of N and P (from the name)
English
Let $R$, $M$, $N$ and $P$ be sets. Then the associator of $N$ and $P$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $N$ and $P$ and the set of tensor products of $M$ and the set of tensor products of $N$ and $P$.
TensorProduct.leftCommdefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$, $M$, $N$ and $P$ be sets. Then $\operatorname{leftComm}$ applied to $R$, $M$, $N$ and $P$ is a linear equivalence of the set of tensor products of $M$ and the set of tensor products of $N$ and $P$ and the set of tensor products of $N$ and the set of tensor products of $M$ and $P$ defined as the composition of the inverse of the associator of $N$ and $P$ and the composition of the congruence of $\operatorname{comm}$ applied to $R$, $M$ and $N$ and $1$ and the associator of $M$ and $P$.
TensorProduct.liddefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{lid}$ applied to $R$ and $M$ is a linear equivalence of the set of tensor products of $R$ and $M$ and $M$.
TensorProduct.lidOfCompatibleSMuldefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$, $A$ and $M$ be sets. Then $\operatorname{lidOfCompatibleSMul}$ applied to $R$, $A$ and $M$ is a linear equivalence of the set of tensor products of $A$ and $M$ and $M$ defined as the composition of the inverse of the equivalence of $A$ and $M$ and $\operatorname{lid}$ applied to $A$ and $M$.
TensorProduct.riddefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$ and $M$ be sets. Then $\operatorname{rid}$ applied to $R$ and $M$ is a linear equivalence of the set of tensor products of $M$ and $R$ and $M$.
TensorProduct.rightCommdefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$, $M$, $N$ and $P$ be sets. Then $\operatorname{rightComm}$ applied to $R$, $M$, $N$ and $P$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $N$ and $P$ and the set of tensor products of the set of tensor products of $M$ and $P$ and $N$.
TensorProduct.tensorTensorTensorAssocdefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantWording
the tensor tensor tensor associator of P and Q (from the name)
English
Let $R$, $M$, $N$, $P$ and $Q$ be sets. Then the tensor tensor tensor associator of $P$ and $Q$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$ and the set of tensor products of the set of tensor products of $M$ and the set of tensor products of $N$ and $P$ and $Q$ defined as the composition of the inverse of the associator of $P$ and $Q$ and the congruence of the associator of $N$ and $P$ and $1$.
TensorProduct.tensorTensorTensorCommdefMathlib.LinearAlgebra.TensorProduct.Associator, function or constantEnglish
Let $R$, $M$, $N$, $P$ and $Q$ be sets. Then $\operatorname{tensorTensorTensorComm}$ applied to $R$, $M$, $N$, $P$ and $Q$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$ and the set of tensor products of the set of tensor products of $M$ and $P$ and the set of tensor products of $N$ and $Q$ defined as the composition of the composition of the inverse of the associator of $P$ and $Q$ and the congruence of $\operatorname{rightComm}$ applied to $R$, $M$, $N$ and $P$ and the identity map of $R$ and $Q$ and the associator of $N$ and $Q$.
TensorProduct.commdefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantEnglish
Let $R$, $M$ and $N$ be sets. Then $\operatorname{comm}$ applied to $R$, $M$ and $N$ is a linear equivalence of the set of tensor products of $M$ and $N$ and the set of tensor products of $N$ and $M$.
TensorProduct.currydefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the curry of f (from the name)
English
Let $f$ be a linear map of the set of tensor products of $M$ and $N$ and $x_{4}$. Then the curry of $f$ is a linear map of $M$ and the set of linear maps of $N$ and $x_{4}$ defined as $\operatorname{lcurry}$ applied to $x_{3}$, $M$, $N$, $x_{4}$ and $f$.
TensorProduct.equivOfCompatibleSMuldefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the equivalence of M and N (from the name)
English
Let $R$, $A$, $S$, $M$ and $N$ be sets. Then the equivalence of $M$ and $N$ is a linear equivalence of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $N$.
TensorProduct.lcurrydefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantEnglish
Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $M$, $N$ and $x_{4}$ be sets. Then $\operatorname{lcurry}$ applied to $x_{3}$, $M$, $N$ and $x_{4}$ is a linear map of the set of linear maps of the set of tensor products of $M$ and $N$ and $x_{4}$ and the set of linear maps of $M$ and the set of linear maps of $N$ and $x_{4}$ defined as $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of $x_{3}$.
TensorProduct.liftdefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the lift of #1 (from the name)
English
Let $\mathrm{f'}$ be a linear map of $M$ and the set of linear maps of $N$ and $x_{4}$. Then the lift of $\mathrm{f'}$ is a linear map of the set of tensor products of $M$ and $N$ and $x_{4}$.
TensorProduct.lift.equivdefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the equivalence of x3 (from the name)
English
Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $M$, $N$ and $x_{4}$ be sets. Then the equivalence of $x_{3}$ is a linear equivalence of the set of linear maps of $M$ and the set of linear maps of $N$ and $x_{4}$ and the set of linear maps of the set of tensor products of $M$ and $N$ and $x_{4}$.
TensorProduct.liftAddHomdefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the lift additive homomorphism of f and hf (from the name)
English
Let $f$ be an additive monoid homomorphism of $M$ and the set of additive monoid homomorphisms of $N$ and $P$ such that for all elements $r$ of $R$, for all elements $m$ of $M$, for all elements $n$ of $N$, $\EqtMACRoH {\operatorname{coe} (f , \HSMulhSMulMACRoAL {r}{m}, n)}{\operatorname{coe} (f , m , \HSMulhSMulMACRoAL {r}{n})}$. Then the lift additive homomorphism of $f$ and $\mathrm{hf}$ is an additive monoid homomorphism of the set of tensor products of $M$ and $N$ and $P$.
TensorProduct.mapOfCompatibleSMuldefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantWording
the map of M and N (from the name)
English
Let $R$, $A$, $S$, $M$ and $N$ be sets. Then the map of $M$ and $N$ is a linear map of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $N$.
TensorProduct.uncurrydefMathlib.LinearAlgebra.TensorProduct.Basic, function or constantEnglish
Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $M$, $N$ and $x_{4}$ be sets. Then $\operatorname{uncurry}$ applied to $x_{3}$, $M$, $N$ and $x_{4}$ is a linear map of the set of linear maps of $M$ and the set of linear maps of $N$ and $x_{4}$ and the set of linear maps of the set of tensor products of $M$ and $N$ and $x_{4}$.
Module.Basis.baseChangedefMathlib.LinearAlgebra.TensorProduct.Basis, function or constantWording
the base change of S and b (from the name)
English
Let $S$ be a set. Let $b$ be a basis of $R$ and $M$. Then the base change of $S$ and $b$ is a basis of $S$ and the set of tensor products of $S$ and $M$ defined as the reindexing of the tensor product of the singleton of $\mathrm{Unit}$ and $S$ and $b$ and $\operatorname{punitProd}$ applied to $x$.
Module.Basis.tensorProductdefMathlib.LinearAlgebra.TensorProduct.Basis, function or constantWording
the tensor product of b and c (from the name)
English
Let $b$ be a basis of $S$ and $M$. Let $c$ be a basis of $R$ and $N$. Then the tensor product of $b$ and $c$ is a basis of $S$ and the set of tensor products of $M$ and $N$ defined as the map of the basis single one and the inverse of the composition of the congruence of the representation of $b$ and the representation of $c$ and the composition of the tensor product of $R$ and $\operatorname{lcongr}$ applied to the identity of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\operatorname{rid}$ applied to $R$, $S$ and $S$.
TensorProduct.equivFinsuppOfBasisLeftdefMathlib.LinearAlgebra.TensorProduct.Basis, function or constantWording
the equivalence finitely supported function of x7 (from the name)
English
Let $x_{7}$ be a basis of $R$ and $M$. Then the equivalence finitely supported function of $x_{7}$ is a linear equivalence of the set of tensor products of $M$ and $N$ and $\FinsuppMACRoQ {x}{N}$ defined as the composition of $\operatorname{comm}$ applied to $R$, $M$ and $N$ and the equivalence finitely supported function of $x_{7}$.
TensorProduct.equivFinsuppOfBasisRightdefMathlib.LinearAlgebra.TensorProduct.Basis, function or constantWording
the equivalence finitely supported function of x7 (from the name)
English
Let $x_{7}$ be a basis of $R$ and $N$. Then the equivalence finitely supported function of $x_{7}$ is a linear equivalence of the set of tensor products of $M$ and $N$ and $\FinsuppMACRoQ {x}{M}$ defined as the composition of the tensor of $M$ and the representation of $x_{7}$ and the right finitely supported function scalar of $M$ and $x$.
DirectSum.decomposeTensordefMathlib.LinearAlgebra.TensorProduct.Decomposition, function or constantEnglish
Let $x_{4}$ be a function from elements of $x$ to submodules of $R$ and $M$. Let $N$ be a set. Let $i$ be an element of $x$. Then $\operatorname{decomposeTensor}$ applied to $x_{4}$, $N$ and $i$ is a submodule of $R$ and the set of tensor products of $M$ and $N$ defined as the range of the tensor of $N$ and the subtype of $x_{4}$ applied to $i$.
DirectSum.decomposeTensorEquivdefMathlib.LinearAlgebra.TensorProduct.Decomposition, function or constantEnglish
Let $x_{4}$ be a function from elements of $x$ to submodules of $R$ and $M$. Let $N$ be a set. Let $i$ be an element of $x$. Then $\operatorname{decomposeTensorEquiv}$ applied to $x_{4}$, $N$ and $i$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{4} (i)}{x_{9}})}$ and $N$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{decomposeTensor} (x_{4} , N , i)}{x_{10}})}$ defined as the linear equivalence of the tensor of $N$ and the subtype of $x_{4}$ applied to $i$ and $\mathrm{DirectSum\_\_subtype\_rTensor\_injective}$ applied to $x_{4}$, $N$ and $i$.
TensorProductdefMathlib.LinearAlgebra.TensorProduct.Defs, typeWording
tensor product of M and N (from the name)
English
Let $R$, $M$ and $N$ be sets. Then a tensor product of $M$ and $N$ is an element of the function that maps $R$, $M$ and $N$ to the set of quotients of the additive congruence relation generator of $\operatorname{Eqv}$ applied to $R$, $M$ and $N$.
TensorProduct.CompatibleSMulclassMathlib.LinearAlgebra.TensorProduct.Defs, predicateEnglish
Let $R$, $\mathrm{R'}$, $M$ and $N$ be sets. Then we can say that $\operatorname{CompatibleSMul}$ holds for $R$, $\mathrm{R'}$, $M$ and $N$.
TensorProduct.EqvinductiveMathlib.LinearAlgebra.TensorProduct.Defs, predicateEnglish
Let $R$, $M$ and $N$ be sets. Let $x_{5}$ and $x_{6}$ be free additive monoids of $\mathrm{Prod}$ applied to $M$ and $N$. Then we can say that $\operatorname{Eqv}$ holds for $R$, $M$, $N$, $x_{5}$ and $x_{6}$.
TensorProduct.mkdefMathlib.LinearAlgebra.TensorProduct.Defs, function or constantEnglish
Let $R$, $M$ and $N$ be sets. Then $\operatorname{mk}$ applied to $R$, $M$ and $N$ is a linear map of $M$ and the set of linear maps of $N$ and the set of tensor products of $M$ and $N$.
TensorProduct.tmuldefMathlib.LinearAlgebra.TensorProduct.Defs, function or constantEnglish
Let $R$ be a set. Let $m$ be an element of $M$. Let $n$ be an element of $N$. Then $\operatorname{tmul}$ applied to $R$, $m$ and $n$ is a tensor product of $M$ and $N$ defined as $\operatorname{mk'}$ applied to the additive congruence relation generator of $\operatorname{Eqv}$ applied to $R$, $M$ and $N$ and $\operatorname{of}$ applied to $\ProdmkMACRoU {m}{n}$.
TensorProduct.directLimitLeftdefMathlib.LinearAlgebra.TensorProduct.DirectLimit, function or constantWording
the left direct limit of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Let $M$ be a set. Then the left direct limit of $i$ and $j$ is a linear equivalence of the set of tensor products of the set of direct limits of $G$ and $f$ and $M$ and the set of direct limits of the function that maps $x_{8}$ to the set of tensor products of $G$ applied to $x_{8}$ and $M$ and the function that maps $x_{9}$, $x_{10}$ and $h$ to the tensor of $M$ and $f$ applied to $x_{9}$, $x_{10}$ and $h$.
TensorProduct.directLimitRightdefMathlib.LinearAlgebra.TensorProduct.DirectLimit, function or constantWording
the right direct limit of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Let $M$ be a set. Then the right direct limit of $i$ and $j$ is a linear equivalence of the set of tensor products of $M$ and the set of direct limits of $G$ and $f$ and the set of direct limits of the function that maps $x_{8}$ to the set of tensor products of $M$ and $G$ applied to $x_{8}$ and the function that maps $x_{9}$, $x_{10}$ and $h$ to the tensor of $M$ and $f$ applied to $x_{9}$, $x_{10}$ and $h$.
TensorProduct.fromDirectLimitdefMathlib.LinearAlgebra.TensorProduct.DirectLimit, function or constantEnglish
Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Let $M$ be a set. Then $\operatorname{fromDirectLimit}$ applied to $i$, $j$, $f$ and $M$ is a linear map of the set of direct limits of the function that maps $x_{8}$ to the set of tensor products of $G$ applied to $x_{8}$ and $M$ and the function that maps $x_{9}$, $x_{10}$ and $h$ to the tensor of $M$ and $f$ applied to $x_{9}$, $x_{10}$ and $h$ and the set of tensor products of the set of direct limits of $G$ and $f$ and $M$.
TensorProduct.toDirectLimitdefMathlib.LinearAlgebra.TensorProduct.DirectLimit, function or constantWording
the direct limit of f and i (from the name)
English
Let $f$ be a function from elements $i$ of $x_{1}$ and elements $j$ of $x_{1}$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (i , j)$ to linear maps of $G$ applied to $i$ and $G$ applied to $j$. Let $M$ be a set. Then the direct limit of $i$ and $j$ is a linear map of the set of tensor products of the set of direct limits of $G$ and $f$ and $M$ and the set of direct limits of the function that maps $x_{8}$ to the set of tensor products of $G$ applied to $x_{8}$ and $M$ and the function that maps $x_{9}$, $x_{10}$ and $h$ to the tensor of $M$ and $f$ applied to $x_{9}$, $x_{10}$ and $h$.
Algebra.TensorProduct.equivFinsuppOfBasisdefMathlib.LinearAlgebra.TensorProduct.Free, function or constantWording
the equivalence finitely supported function of A and b (from the name)
English
Let $A$ be a set. Let $b$ be a basis of $R$ and $V$. Then the equivalence finitely supported function of $A$ and $b$ is a linear equivalence of the set of tensor products of $A$ and $V$ and $\FinsuppMACRoQ {x_{5}}{A}$ defined as the composition of the base change of the representation of $b$ and the right finitely supported function scalar of $A$ and $x_{5}$.
Algebra.TensorProduct.equivPiOfFiniteBasisdefMathlib.LinearAlgebra.TensorProduct.Free, function or constantWording
the equivalence product of A and b (from the name)
English
Let $A$ be a set. Let $b$ be a basis of $R$ and $V$. Then the equivalence product of $A$ and $b$ is a linear equivalence of the set of tensor products of $A$ and $V$ and the set of functions from elements of $x_{5}$ to elements of $A$ defined as the composition of the base change of the equivalence function of $b$ and the right product scalar of $A$ and $x_{5}$.
TensorProduct.gradedCommdefMathlib.LinearAlgebra.TensorProduct.Graded.External, function or constantEnglish
Let $R$ be a set. Let $x_{4}$ and $x_{5}$ be functions from elements of $x$ to sets. Then $\operatorname{gradedComm}$ applied to $R$, $x_{4}$ and $x_{5}$ is a linear equivalence of the set of tensor products of the set of direct sums of $x$ and the function that maps $i$ to $x_{4}$ applied to $i$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $x_{5}$ applied to $i_{1}$ and the set of tensor products of the set of direct sums of $x$ and the function that maps $i_{2}$ to $x_{5}$ applied to $i_{2}$ and the set of direct sums of $x$ and the function that maps $i_{3}$ to $x_{4}$ applied to $i_{3}$ defined as the composition of the composition of the direct sum of $x_{4}$ and $x_{5}$ and the linear equivalence of $\operatorname{gradedCommAux}$ applied to $R$, $x_{4}$ and $x_{5}$ and $\operatorname{gradedCommAux}$ applied to $R$, $x_{5}$ and $x_{4}$ and the inverse of the direct sum of $x_{5}$ and $x_{4}$.
TensorProduct.gradedMuldefMathlib.LinearAlgebra.TensorProduct.Graded.External, function or constantWording
the graded product of x4 and x5 (from the name)
English
Let $R$ be a set. Let $x_{4}$ and $x_{5}$ be functions from elements of $x$ to sets. Then the graded product of $x_{4}$ and $x_{5}$ is a linear map of the set of tensor products of the set of direct sums of $x$ and $x_{4}$ and the set of direct sums of $x$ and $x_{5}$ and the set of linear maps of the set of tensor products of the set of direct sums of $x$ and $x_{4}$ and the set of direct sums of $x$ and $x_{5}$ and the set of tensor products of the set of direct sums of $x$ and $x_{4}$ and the set of direct sums of $x$ and $x_{5}$ defined as $\operatorname{proj0}$ applied to $\mathrm{TensorProduct\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_TensorProduct\_\_Graded\_\_External\_\_2950040696\_\_\_hygCtx\_\_\_hyg\_\_8}$, $R$, $x_{4}$ and $x_{5}$.