Definitions: Mathlib.LinearAlgebra, part 5 of 5

graded tensor product of x8 and x9 (from the name)

Let $R$ be a set. Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then a graded tensor product of $x_{8}$ and $x_{9}$ is an element of the function that maps $R$, $x_{8}$ and $x_{9}$ to the set of tensor products of $A$ and $B$.

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then $\operatorname{comm}$ applied to $x_{8}$ and $x_{9}$ is an algebra isomorphism of the set of graded tensor products of $x_{8}$ and $x_{9}$ and the set of graded tensor products of $x_{9}$ and $x_{8}$.

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then $\operatorname{includeLeft}$ applied to $x_{8}$ and $x_{9}$ is an algebra homomorphism of $A$ and the set of graded tensor products of $x_{8}$ and $x_{9}$.

the ring morphism of x8 and x9 (from the docstring)

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then the ring morphism of $x_{8}$ and $x_{9}$ is a ring homomorphism of $A$ and the set of graded tensor products of $x_{8}$ and $x_{9}$.

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then $\operatorname{includeRight}$ applied to $x_{8}$ and $x_{9}$ is an algebra homomorphism of $B$ and the set of graded tensor products of $x_{8}$ and $x_{9}$.

the lift of f and g (from the name)

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Let $f$ be an algebra homomorphism of $A$ and $C$. Let $g$ be an algebra homomorphism of $B$ and $C$ such that for all elements $i$ and $j$ of $x$, for all elements $a$ of $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {x_{8} (i)}{x_{16}})}$, for all elements $b$ of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {x_{9} (j)}{x_{15}})}$, $\EqtMACRoH {f (a)\times g (b)}{\HSMulhSMulMACRoAL {(\operatorname{neg} (1)^ {j \times i})}{(g (b)\times f (a))}}$. Then the lift of $f$ and $g$ is an algebra homomorphism of the set of graded tensor products of $x_{8}$ and $x_{9}$ and $C$.

the lift equivalence of x8 and x9 (from the name)

Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then the lift equivalence of $x_{8}$ and $x_{9}$ is an equivalence from $\SubtypeSet {\mathrm{fg}}{\mathrm{forall} (x , \lambda i . \mathrm{forall} (x , \lambda j . \mathrm{forall} (\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {x_{8} (i)}{x_{16}})}, \lambda a . \mathrm{forall} (\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {x_{9} (j)}{x_{15}})}, \lambda b . \EqtMACRoH {(\operatorname{fst} (\mathrm{fg} , a)\times \operatorname{snd} (\mathrm{fg} , b))}{(\HSMulhSMulMACRoAL {(\operatorname{neg} (1)^ {j \times i})}{(\operatorname{snd} (\mathrm{fg} , b)\times \operatorname{fst} (\mathrm{fg} , a))})}))))}$ to the set of algebra homomorphisms of the set of graded tensor products of $x_{8}$ and $x_{9}$ and $C$.

Let $R$ be a set. Let $x_{8}$ be a function from elements of $x$ to submodules of $R$ and $A$. Let $x_{9}$ be a function from elements of $x$ to submodules of $R$ and $B$. Then $\operatorname{of}$ applied to $R$, $x_{8}$ and $x_{9}$ is a linear equivalence of the set of tensor products of $A$ and $B$ and the set of graded tensor products of $x_{8}$ and $x_{9}$ defined as the identity map of $R$ and the set of tensor products of $A$ and $B$.

Let $R$ be a set. Let $a$ be an element of $A$. Let $b$ be an element of $B$. Then $\operatorname{tmul}$ applied to $R$, $a$ and $b$ is a graded tensor product of $x_{8}$ and $x_{9}$ defined as $\operatorname{of}$ applied to $R$, $x_{8}$, $x_{9}$ and $\operatorname{tmul}$ applied to $R$, $a$ and $b$.

the lift base change of A and l (from the name)

Let $A$ be a set. Let $l$ be a linear map of $M$ and $N$. Then the lift base change of $A$ and $l$ is a linear map of the set of tensor products of $A$ and $M$ and $N$ defined as $\operatorname{liftBaseChangeEquiv}$ applied to $A$ and $l$.

the lift base change equivalence of A (from the name)

Let $A$ be a set. Then the lift base change equivalence of $A$ is a linear equivalence of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of tensor products of $A$ and $M$ and $N$ defined as the composition of the inverse of $\operatorname{ringLmapEquivSelf}$ applied to $A$, $A$ and the set of linear maps of $M$ and $N$ and the equivalence of $M$ and $N$.

the tensor of M and f (from the name)

Let $M$ be a set. Let $f$ be a linear equivalence of $N$ and $P$. Then the tensor of $M$ and $f$ is a linear equivalence of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $P$ defined as the congruence of the identity map of $R$ and $M$ and $f$.

the tensor of M and f (from the name)

Let $M$ be a set. Let $f$ be a linear equivalence of $N$ and $P$. Then the tensor of $M$ and $f$ is a linear equivalence of the set of tensor products of $N$ and $M$ and the set of tensor products of $P$ and $M$ defined as the congruence of $f$ and the identity map of $R$ and $M$.

the tensor of M and f (from the name)

Let $M$ be a set. Let $f$ be a linear map of $N$ and $P$. Then the tensor of $M$ and $f$ is a linear map of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $P$ defined as the tensor product of the identity and $f$.

the tensor homomorphism of M (from the name)

Let $M$ be a set. Then the tensor homomorphism of $M$ is a linear map of the set of linear maps of $N$ and $P$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $P$.

the tensor of M and f (from the name)

Let $M$ be a set. Let $f$ be a linear map of $N$ and $P$. Then the tensor of $M$ and $f$ is a linear map of the set of tensor products of $N$ and $M$ and the set of tensor products of $P$ and $M$ defined as the tensor product of $f$ and the identity.

the tensor homomorphism of M (from the name)

Let $M$ be a set. Then the tensor homomorphism of $M$ is a linear map of the set of linear maps of $N$ and $P$ and the set of linear maps of the set of tensor products of $N$ and $M$ and the set of tensor products of $P$ and $M$.

the congruence of f and g (from the name)

Let $f$ be a linear equivalence of $M$ and $x_{4}$. Let $g$ be a linear equivalence of $N$ and $x_{5}$. Then the congruence of $f$ and $g$ is a linear equivalence of the set of tensor products of $M$ and $N$ and the set of tensor products of $x_{4}$ and $x_{5}$.

the homomorphism tensor homomorphism map of x3 (from the name)

Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $M$, $N$, $x_{4}$ and $x_{5}$ be sets. Then the homomorphism tensor homomorphism map of $x_{3}$ is a linear map of the set of tensor products of the set of linear maps of $M$ and $x_{4}$ and the set of linear maps of $N$ and $x_{5}$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $x_{4}$ and $x_{5}$ defined as the lift of the map bilinear of $x_{3}$.

the tensor homomorphism to homomorphism tensor of x3 (from the name)

Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $P$, $x_{4}$ and $x_{5}$ be sets. Then the tensor homomorphism to homomorphism tensor of $x_{3}$ is a linear map of the set of tensor products of $x_{4}$ and the set of linear maps of $P$ and $x_{5}$ and the set of linear maps of $P$ and the set of tensor products of $x_{4}$ and $x_{5}$ defined as the lift of the composition of $\operatorname{llcomp}$ applied to $x$, $P$, $x_{5}$ and the set of tensor products of $x_{4}$ and $x_{5}$ and $\operatorname{mk}$ applied to $x$, $x_{4}$ and $x_{5}$.

the tensor product of f and g (from the docstring)

Let $f$ be a linear map of $M$ and $x_{4}$. Let $g$ be a linear map of $N$ and $x_{5}$. Then the tensor product of $f$ and $g$ is a linear map of the set of tensor products of $M$ and $N$ and the set of tensor products of $x_{4}$ and $x_{5}$ defined as the lift of the composition of the complement of $\operatorname{mk}$ applied to $x$, $x_{4}$ and $x_{5}$ and $g$ and $f$.

the map bilinear of x3 (from the name)

Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $M$, $N$, $x_{4}$ and $x_{5}$ be sets. Then the map bilinear of $x_{3}$ is a linear map of the set of linear maps of $M$ and $x_{4}$ and the set of linear maps of the set of linear maps of $N$ and $x_{5}$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $x_{4}$ and $x_{5}$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $x$, $\operatorname{map}$, $\mathrm{TensorProduct\_\_map\_add\_left}$, $\mathrm{TensorProduct\_\_map\_smul\_left}$, $\mathrm{TensorProduct\_\_map\_add\_right}$ and $\mathrm{TensorProduct\_\_map\_smul\_right}$.

the map inclusion of p and q (from the name)

Let $p$ be a submodule of $R$ and $P$. Let $q$ be a submodule of $R$ and $Q$. Then the map inclusion of $p$ and $q$ is a linear map of the set of tensor products of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {q}{x_{6}})}$ and the set of tensor products of $P$ and $Q$ defined as the tensor product of the subtype of $p$ and the subtype of $q$.

the map of f and g (from the name)

Let $f$ be a linear map of $M$ and the set of linear maps of $x_{7}$ and $x_{8}$. Let $g$ be a linear map of $N$ and the set of linear maps of $x_{9}$ and $x_{10}$. Then the map of $f$ and $g$ is a linear map of the set of tensor products of $M$ and $N$ and the set of linear maps of the set of tensor products of $x_{7}$ and $x_{9}$ and the set of tensor products of $x_{8}$ and $x_{10}$ defined as the composition of the homomorphism tensor homomorphism map of $x_{5}$ and the tensor product of $f$ and $g$.

the tensor homomorphism to homomorphism tensor of x3 (from the name)

Let $x_{3}$ be a ring homomorphism of $R$ and $x$. Let $P$, $x_{4}$ and $x_{5}$ be sets. Then the tensor homomorphism to homomorphism tensor of $x_{3}$ is a linear map of the set of tensor products of the set of linear maps of $P$ and $x_{4}$ and $x_{5}$ and the set of linear maps of $P$ and the set of tensor products of $x_{4}$ and $x_{5}$ defined as the lift of the flip of the composition of $\operatorname{llcomp}$ applied to $x$, $P$, $x_{4}$ and the set of tensor products of $x_{4}$ and $x_{5}$ and the flip of $\operatorname{mk}$ applied to $x$, $x_{4}$ and $x_{5}$.

the opposite algebra isomorphism of A and B (from the name)

Let $R$, $S$, $A$ and $B$ be sets. Then the opposite algebra isomorphism of $A$ and $B$ is an algebra isomorphism of the set of tensor products of the set of multiplicative opposites of $A$ and the set of multiplicative opposites of $B$ and the set of multiplicative opposites of the set of tensor products of $A$ and $B$.

the left product of M (from the name)

Let $R$ and $N$ be sets. Let $M$ be a function from elements of $x_{3}$ to sets. Then the left product of $M$ is a linear equivalence of the set of tensor products of the set of functions from elements $i$ of $x_{3}$ to elements of $M$ applied to $i$ and $N$ and the set of functions from elements $i_{1}$ of $x_{3}$ to tensor products of $M$ applied to $i_{1}$ and $N$ defined as the composition of the composition of $\operatorname{comm}$ applied to $R$, the set of functions from elements $i$ of $x_{3}$ to elements of $M$ applied to $i$ and $N$ and the right product of $M$ and the right product congruence of the function that maps $x_{8}$ to $\operatorname{comm}$ applied to $R$, $N$ and $M$ applied to $x_{8}$.

the right product of M (from the name)

Let $R$, $S$ and $N$ be sets. Let $M$ be a function from elements of $x_{6}$ to sets. Then the right product of $M$ is a linear equivalence of the set of tensor products of $N$ and the set of functions from elements $i$ of $x_{6}$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to tensor products of $N$ and $M$ applied to $i_{1}$.

the product right homomorphism of M (from the name)

Let $R$, $S$ and $N$ be sets. Let $M$ be a function from elements of $x_{6}$ to sets. Then the product right homomorphism of $M$ is a linear map of the set of tensor products of $N$ and the set of functions from elements $i$ of $x_{6}$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to tensor products of $N$ and $M$ applied to $i_{1}$ defined as the lift of $\operatorname{piRightHomBil}$ applied to $R$, $S$, $N$ and $M$.

Let $R$, $S$ and $N$ be sets. Let $M$ be a function from elements of $x_{6}$ to sets. Then $\operatorname{piRightHomBil}$ applied to $R$, $S$, $N$ and $M$ is a linear map of $N$ and the set of linear maps of the set of functions from elements $i$ of $x_{6}$ to elements of $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x_{6}$ to tensor products of $N$ and $M$ applied to $i_{1}$.

the product right inverse of M (from the name)

Let $R$, $S$ and $N$ be sets. Let $M$ be a function from elements of $x_{6}$ to sets. Then the product right inverse of $M$ is a linear map of the set of functions from elements $i$ of $x_{6}$ to tensor products of $N$ and $M$ applied to $i$ and the set of tensor products of $N$ and the set of functions from elements $i_{1}$ of $x_{6}$ to elements of $M$ applied to $i_{1}$ defined as $\operatorname{lsum}$ applied to $S$, the function that maps $i_{5}$ to the set of tensor products of $N$ and $M$ applied to $i_{5}$, $S$ and the function that maps $i_{6}$ to the map of the identity and $\operatorname{single}$ applied to $R$, $M$ and $i_{6}$.

the right product scalar of N and x6 (from the name)

Let $R$, $S$, $N$ and $x_{6}$ be sets. Then the right product scalar of $N$ and $x_{6}$ is a linear equivalence of the set of tensor products of $N$ and the set of functions from elements of $x_{6}$ to elements of $R$ and the set of functions from elements of $x_{6}$ to elements of $N$.

the product scalar right homomorphism of N and x6 (from the name)

Let $R$, $S$, $N$ and $x_{6}$ be sets. Then the product scalar right homomorphism of $N$ and $x_{6}$ is a linear map of the set of tensor products of $N$ and the set of functions from elements of $x_{6}$ to elements of $R$ and the set of functions from elements of $x_{6}$ to elements of $N$ defined as the lift of $\operatorname{piScalarRightHomBil}$ applied to $R$, $S$, $N$ and $x_{6}$.

Let $R$, $S$, $N$ and $x_{6}$ be sets. Then $\operatorname{piScalarRightHomBil}$ applied to $R$, $S$, $N$ and $x_{6}$ is a linear map of $N$ and the set of linear maps of the set of functions from elements of $x_{6}$ to elements of $R$ and the set of functions from elements of $x_{6}$ to elements of $N$.

the product scalar right inverse of N and x6 (from the name)

Let $R$, $S$, $N$ and $x_{6}$ be sets. Then the product scalar right inverse of $N$ and $x_{6}$ is a linear map of the set of functions from elements of $x_{6}$ to elements of $N$ and the set of tensor products of $N$ and the set of functions from elements of $x_{6}$ to elements of $R$.

the left product of x1 and x2 (from the name)

Let $R$, $S$, $x$, $x_{1}$ and $x_{2}$ be sets. Then the left product of $x_{1}$ and $x_{2}$ is a linear equivalence of the set of tensor products of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to the set of tensor products of $x$ and $x_{2}$ and the set of tensor products of $x_{1}$ and $x_{2}$.

the right product of x1 and x2 (from the name)

Let $R$, $S$, $x$, $x_{1}$ and $x_{2}$ be sets. Then the right product of $x_{1}$ and $x_{2}$ is a linear equivalence of the set of tensor products of $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to the set of tensor products of $x$ and $x_{1}$ and the set of tensor products of $x$ and $x_{2}$.

the quotient map equivalence tensor quotient of S (from the name)

Let $S$ be a set. Then the quotient map equivalence tensor quotient of $S$ is a linear equivalence of the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$ and the set of tensor products of $S$ and the set of quotients of $R$ and $I$.

the tensor quotient equivalence of n (from the name)

Let $A$, $B$ and $M$ be sets. Let $n$ be a submodule of $B$ and $N$. Then the tensor quotient equivalence of $n$ is a linear equivalence of the set of tensor products of $M$ and the set of quotients of $N$ and $n$ and the set of quotients of the set of tensor products of $M$ and $N$ and the range of $\operatorname{lTensor}$ applied to $A$, $M$ and $\operatorname{restrictScalars}$ applied to $R$ and the subtype of $n$.

the quotient tensor equivalence quotient product of M and I (from the name)

Let $M$ be a set. Let $I$ be an ideal of $R$. Then the quotient tensor equivalence quotient product of $M$ and $I$ is a linear equivalence of the set of tensor products of the set of quotients of $R$ and $I$ and $M$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$.

the quotient tensor equivalence of N and m (from the name)

Let $N$ be a set. Let $m$ be a submodule of $R$ and $M$. Then the quotient tensor equivalence of $N$ and $m$ is a linear equivalence of the set of tensor products of the set of quotients of $M$ and $m$ and $N$ and the set of quotients of the set of tensor products of $M$ and $N$ and the range of the tensor product of the subtype of $m$ and the identity.

the quotient tensor quotient equivalence of m and n (from the name)

Let $m$ be a submodule of $R$ and $M$. Let $n$ be a submodule of $R$ and $N$. Then the quotient tensor quotient equivalence of $m$ and $n$ is a linear equivalence of the set of tensor products of the set of quotients of $M$ and $m$ and the set of quotients of $N$ and $n$ and the set of quotients of the set of tensor products of $M$ and $N$ and the maximum of the range of the tensor product of the subtype of $m$ and the identity and the range of the tensor product of the identity and the subtype of $n$.

the tensor quotient equivalence quotient product of M and I (from the name)

Let $M$ be a set. Let $I$ be an ideal of $R$. Then the tensor quotient equivalence quotient product of $M$ and $I$ is a linear equivalence of the set of tensor products of $M$ and the set of quotients of $R$ and $I$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$ defined as the composition of $\operatorname{comm}$ applied to $R$, $M$ and the set of quotients of $R$ and $I$ and the quotient tensor equivalence quotient product of $M$ and $I$.

the tensor quotient map multiplicative equivalence tensor quotient of I (from the name)

Let $M$ and $S$ be sets. Let $I$ be an ideal of $R$. Then the tensor quotient map multiplicative equivalence tensor quotient of $I$ is a linear equivalence of the set of quotients of the set of tensor products of $S$ and $M$ and $\HSMulhSMulMACRoAL {\operatorname{map} (\operatorname{algebraMap} (R , S), I)}{\operatorname{top}}$ and the set of tensor products of $S$ and the set of quotients of $M$ and $\HSMulhSMulMACRoAL {I}{\operatorname{top}}$ defined as the composition of the composition of the composition of the composition of the composition of the composition of the inverse of the tensor quotient equivalence quotient product of the set of tensor products of $S$ and $M$ and the map of the algebra map of $R$ and $S$ and $I$ and $\operatorname{comm}$ applied to $S$, the set of tensor products of $S$ and $M$ and the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$ and $\operatorname{cancelBaseChange}$ applied to $R$, $S$, $S$, the set of quotients of $S$ and the map of the algebra map of $R$ and $S$ and $I$ and $M$ and the congruence of the quotient map equivalence tensor quotient of $S$ and the identity map of $R$ and $M$ and the associator of the set of quotients of $R$ and $I$ and $M$ and the base change of $\operatorname{comm}$ applied to $R$, the set of quotients of $R$ and $I$ and $M$ and the base change of the tensor quotient equivalence quotient product of $M$ and $I$.

the tensor quotient equivalence of M and n (from the name)

Let $M$ be a set. Let $n$ be a submodule of $R$ and $N$. Then the tensor quotient equivalence of $M$ and $n$ is a linear equivalence of the set of tensor products of $M$ and the set of quotients of $N$ and $n$ and the set of quotients of the set of tensor products of $M$ and $N$ and the range of the tensor product of the identity and the subtype of $n$.

the equivalence of hfg and hg (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the equivalence of $\mathrm{hfg}$ and $\mathrm{hg}$ is a linear equivalence of the set of quotients of the set of tensor products of $Q$ and $N$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $Q$ and $P$.

the inverse map in Q (from the docstring)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the inverse map in $Q$ is a linear map of the set of tensor products of $Q$ and $P$ and the set of quotients of the set of tensor products of $Q$ and $N$ and the range of the tensor of $Q$ and $f$.

the inverse map in Q (from the docstring)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{RightInverse}$ holds for $h$ and $\operatorname{coe}$ applied to $g$. Then the inverse map in $Q$ is a linear map of the set of tensor products of $Q$ and $P$ and the set of quotients of the set of tensor products of $Q$ and $N$ and the range of the tensor of $Q$ and $f$.

the linear equivalence of hfg and hgh (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{RightInverse}$ holds for $h$ and $\operatorname{coe}$ applied to $g$. Then the linear equivalence of $\mathrm{hfg}$ and $\mathrm{hgh}$ is a linear equivalence of the set of quotients of the set of tensor products of $Q$ and $N$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $Q$ and $P$.

the tensor of Q and hfg (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Then the tensor of $Q$ and $\mathrm{hfg}$ is a linear map of the set of quotients of the set of tensor products of $Q$ and $N$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $Q$ and $P$.

the equivalence of hfg and hg (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the equivalence of $\mathrm{hfg}$ and $\mathrm{hg}$ is a linear equivalence of the set of quotients of the set of tensor products of $N$ and $Q$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $P$ and $Q$.

the inverse map in Q (from the docstring)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Then the inverse map in $Q$ is a linear map of the set of tensor products of $P$ and $Q$ and the set of quotients of the set of tensor products of $N$ and $Q$ and the range of the tensor of $Q$ and $f$.

the inverse map in Q (from the docstring)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{RightInverse}$ holds for $h$ and $\operatorname{coe}$ applied to $g$. Then the inverse map in $Q$ is a linear map of the set of tensor products of $P$ and $Q$ and the set of quotients of the set of tensor products of $N$ and $Q$ and the range of the tensor of $Q$ and $f$.

the linear equivalence of hfg and hgh (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{RightInverse}$ holds for $h$ and $\operatorname{coe}$ applied to $g$. Then the linear equivalence of $\mathrm{hfg}$ and $\mathrm{hgh}$ is a linear equivalence of the set of quotients of the set of tensor products of $N$ and $Q$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $P$ and $Q$.

the tensor of Q and hfg (from the name)

Let $Q$ be a set. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Then the tensor of $Q$ and $\mathrm{hfg}$ is a linear map of the set of quotients of the set of tensor products of $N$ and $Q$ and the range of the tensor of $Q$ and $f$ and the set of tensor products of $P$ and $Q$.

Let $R$, $S$ and $T$ be sets. Then $\operatorname{algEquivIncludeRange}$ applied to $R$, $S$ and $T$ is an algebra isomorphism of the set of tensor products of $S$ and $T$ and the set of tensor products of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{includeLeft})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{includeRight})}{x_{6}})}$.

Let $R$, $S$ and $T$ be sets. Then $\operatorname{linearEquivIncludeRange}$ applied to $R$, $S$ and $T$ is a linear equivalence of the set of tensor products of $S$ and $T$ and the set of tensor products of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{includeLeft})}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{includeRight})}{x_{6}})}$.

the tensor bottom of A (from the name)

Let $A$ be a subalgebra of $R$ and $S$. Then the tensor bottom of $A$ is an algebra isomorphism of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {A}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {A}{x_{5}})}$.

the multiplicative map of A and B (from the name)

Let $A$ and $B$ be subalgebras of $R$ and $S$. Then the multiplicative map of $A$ and $B$ is an algebra homomorphism of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {B}{x_{4}})}$ and $S$ defined as the product map of the value of $A$ and the value of $B$.

the multiplicative map of A and B (from the name)

Let $A$ and $B$ be subalgebras of $R$ and $S$. Then the multiplicative map of $A$ and $B$ is an algebra homomorphism of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {B}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {A}{B})}{x_{5}})}$ defined as the composition of the algebra homomorphism of the equivalence of the range of the multiplicative map of $A$ and $B$ and $\MaxmaxMACRoAF {A}{B}$ and $\operatorname{rangeRestrict}$ applied to the multiplicative map of $A$ and $B$.

the tensor bottom of A (from the name)

Let $A$ be a subalgebra of $R$ and $S$. Then the tensor bottom of $A$ is an algebra isomorphism of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {A}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {A}{x_{5}})}$.

the tensor one of N (from the name)

Let $N$ be a submodule of $R$ and $S$. Then the tensor one of $N$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$.

the tensor one of N (from the name)

Let $N$ be a submodule of $R$ and $S$. Then the tensor one of $N$ is a linear map of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$.

the multiplicative map of M and N (from the name)

Let $M$ and $N$ be submodules of $R$ and $S$. Then the multiplicative map of $M$ and $N$ is a linear map of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ and $S$ defined as the lift of $\mathrm{LinearMap\_\_domRestrict\_u2081\_\_u2082\_}$ applied to the product of $R$ and $S$, $M$ and $N$.

the multiplicative map of M and N (from the name)

Let $M$ and $N$ be submodules of $R$ and $S$. Then the multiplicative map of $M$ and $N$ is a linear map of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(M \times N)}{x_{5}})}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the linear equivalence of the range of the multiplicative map of $M$ and $N$ and $M \times N$ and $\operatorname{rangeRestrict}$ applied to the multiplicative map of $M$ and $N$.

the tensor one of M (from the name)

Let $M$ be a submodule of $R$ and $S$. Then the tensor one of $M$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {M}{x_{5}})}$.

the tensor one of M (from the name)

Let $M$ be a submodule of $R$ and $S$. Then the tensor one of $M$ is a linear map of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {M}{x_{5}})}$.

the base change of e (from the name)

Let $R$, $A$, $M$ and $N$ be sets. Let $e$ be a linear equivalence of $M$ and $N$. Then the base change of $e$ is a linear equivalence of the set of tensor products of $A$ and $M$ and the set of tensor products of $A$ and $N$ defined as the congruence of the identity map of $A$ and $A$ and $e$.

the base change of A and f (from the name)

Let $A$ be a set. Let $f$ be a linear map of $M$ and $N$. Then the base change of $A$ and $f$ is a linear map of the set of tensor products of $A$ and $M$ and the set of tensor products of $A$ and $N$ defined as the map of the identity and $f$.

the base change homomorphism of M and N (from the name)

Let $R$, $A$, $M$ and $N$ be sets. Then the base change homomorphism of $M$ and $N$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of the set of tensor products of $A$ and $M$ and the set of tensor products of $A$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{baseChange}$ applied to $A$ and $\mathrm{LinearMap\_\_baseChange\_add}$ and $\mathrm{LinearMap\_\_baseChange\_smul}$.

the base change homomorphism of A and M (from the name)

Let $R$, $A$ and $M$ be sets. Then the base change homomorphism of $A$ and $M$ is an algebra homomorphism of the set of ends of $R$ and $M$ and the set of ends of $A$ and the set of tensor products of $A$ and $M$ defined as the algebra homomorphism of the base change homomorphism of $M$ and $M$.

the base change of A and p (from the name)

Let $A$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the base change of $A$ and $p$ is a submodule of $A$ and the set of tensor products of $A$ and $M$ defined as the range of the base change of $A$ and the subtype of $p$.

the base change of A and p (from the name)

Let $A$ be a set. Let $p$ be a submodule of $R$ and $M$. Then the base change of $A$ and $p$ is a linear map of the set of tensor products of $A$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{baseChange} (A , p)}{x_{6}})}$ defined as $\operatorname{rangeRestrict}$ applied to the base change of $A$ and the subtype of $p$.

the associator of P and Q (from the name)

Let $R$, $A$, $B$, $M$, $P$ and $Q$ be sets. Then the associator of $P$ and $Q$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $P$ and $Q$ and the set of tensor products of $M$ and the set of tensor products of $P$ and $Q$.

Let $R$, $A$, $B$, $M$ and $N$ be sets. Then $\operatorname{cancelBaseChange}$ applied to $R$, $A$, $B$, $M$ and $N$ is a linear equivalence of the set of tensor products of $M$ and the set of tensor products of $A$ and $N$ and the set of tensor products of $M$ and $N$ defined as the composition of the inverse of the associator of $A$ and $N$ and the congruence of $\operatorname{rid}$ applied to $A$, $B$ and $M$ and the identity map of $R$ and $N$.

the congruence of f and g (from the name)

Let $f$ be a linear equivalence of $M$ and $P$. Let $g$ be a linear equivalence of $N$ and $Q$. Then the congruence of $f$ and $g$ is a linear equivalence of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$.

the curry of f (from the name)

Let $f$ be a linear map of the set of tensor products of $M$ and $N$ and $P$. Then the curry of $f$ is a linear map of $M$ and the set of linear maps of $N$ and $P$.

the distributive base change of N and Q (from the name)

Let $R$, $A$, $N$ and $Q$ be sets. Then the distributive base change of $N$ and $Q$ is a linear equivalence of the set of tensor products of $A$ and the set of tensor products of $N$ and $Q$ and the set of tensor products of the set of tensor products of $A$ and $N$ and the set of tensor products of $A$ and $Q$ defined as the inverse of the composition of $\operatorname{cancelBaseChange}$ applied to $R$, $A$, $A$, the set of tensor products of $A$ and $N$ and $Q$ and the associator of $N$ and $Q$.

the homomorphism tensor homomorphism map of P and Q (from the name)

Let $R$, $A$, $B$, $M$, $N$, $P$ and $Q$ be sets. Then the homomorphism tensor homomorphism map of $P$ and $Q$ is a linear map of the set of tensor products of the set of linear maps of $M$ and $P$ and the set of linear maps of $N$ and $Q$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$ defined as the lift of the map bilinear of $P$ and $Q$.

the tensor of A and M (from the name)

Let $A$ and $M$ be sets. Then the tensor of $A$ and $M$ is a linear map of the set of linear maps of $N$ and $Q$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $M$ and $Q$.

Let $R$, $A$, $B$, $M$, $N$ and $P$ be sets. Then $\operatorname{lcurry}$ applied to $R$, $A$, $B$, $M$, $N$ and $P$ is a linear map of the set of linear maps of the set of tensor products of $M$ and $N$ and $P$ and the set of linear maps of $M$ and the set of linear maps of $N$ and $P$.

Let $R$, $A$, $M$, $P$ and $Q$ be sets. Then $\operatorname{leftComm}$ applied to $R$, $A$, $M$, $P$ and $Q$ is a linear equivalence of the set of tensor products of $M$ and the set of tensor products of $P$ and $Q$ and the set of tensor products of $P$ and the set of tensor products of $M$ and $Q$ defined as the composition of the composition of the inverse of the associator of $P$ and $Q$ and the congruence of $\operatorname{comm}$ applied to $A$, $M$ and $P$ and $1$ and the associator of $M$ and $Q$.

the lift of f (from the name)

Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Then the lift of $f$ is a linear map of the set of tensor products of $M$ and $N$ and $P$.

the equivalence of N and P (from the name)

Let $R$, $A$, $B$, $M$, $N$ and $P$ be sets. Then the equivalence of $N$ and $P$ is a linear equivalence of the set of linear maps of $M$ and the set of linear maps of $N$ and $P$ and the set of linear maps of the set of tensor products of $M$ and $N$ and $P$.

the map of f and g (from the name)

Let $f$ be a linear map of $M$ and $P$. Let $g$ be a linear map of $N$ and $Q$. Then the map of $f$ and $g$ is a linear map of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$.

the map bilinear of P and Q (from the name)

Let $R$, $A$, $B$, $M$, $N$, $P$ and $Q$ be sets. Then the map bilinear of $P$ and $Q$ is a linear map of the set of linear maps of $M$ and $P$ and the set of linear maps of the set of linear maps of $N$ and $Q$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $Q$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_'}$ applied to $B$, $R$, $\operatorname{map}$, $\mathrm{TensorProduct\_\_AlgebraTensorModule\_\_map\_add\_left}$, $\mathrm{TensorProduct\_\_AlgebraTensorModule\_\_map\_smul\_left}$, $\mathrm{TensorProduct\_\_AlgebraTensorModule\_\_map\_add\_right}$ and $\mathrm{TensorProduct\_\_AlgebraTensorModule\_\_map\_smul\_right}$.

Let $R$, $A$, $M$ and $N$ be sets. Then $\operatorname{mk}$ applied to $R$, $A$, $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$.

the tensor of R and N (from the name)

Let $R$ and $N$ be sets. Then the tensor of $R$ and $N$ is a linear map of the set of linear maps of $M$ and $P$ and the set of linear maps of the set of tensor products of $M$ and $N$ and the set of tensor products of $P$ and $N$.

Let $R$, $A$ and $M$ be sets. Then $\operatorname{rid}$ applied to $R$, $A$ and $M$ is a linear equivalence of the set of tensor products of $M$ and $R$ and $M$.

Let $R$, $S$, $B$, $M$, $P$ and $Q$ be sets. Then $\operatorname{rightComm}$ applied to $R$, $S$, $B$, $M$, $P$ and $Q$ is a linear equivalence of the set of tensor products of the set of tensor products of $M$ and $P$ and $Q$ and the set of tensor products of the set of tensor products of $M$ and $Q$ and $P$.

Let $R$, $S$, $A$, $B$, $M$, $N$, $P$ and $Q$ be sets. Then $\operatorname{tensorTensorTensorComm}$ applied to $R$, $S$, $A$, $B$, $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 $A$, $S$, $B$, $M$, $N$ and $P$ and the identity map of $R$ and $Q$ and the associator of $N$ and $Q$.

the lift equivalence of M and N (from the name)

Let $R$, $A$, $M$ and $N$ be sets. Then the lift equivalence of $M$ and $N$ is a linear equivalence of $\mathrm{ULift}$ applied to the set of tensor products of $M$ and $N$ and the set of tensor products of $\mathrm{ULift}$ applied to $M$ and $\mathrm{ULift}$ applied to $N$ defined as the composition of the composition of the module equivalence and the congruence of the inverse of the module equivalence and the inverse of the module equivalence and the equivalence of $\mathrm{ULift}$ applied to $M$ and $\mathrm{ULift}$ applied to $N$.

Let $R$, $A$, $B$, $M$, $N$ and $P$ be sets. Then $\operatorname{uncurry}$ applied to $R$, $A$, $B$, $M$, $N$ and $P$ is a linear map of the set of linear maps of $M$ and the set of linear maps of $N$ and $P$ and the set of linear maps of the set of tensor products of $M$ and $N$ and $P$.

Let $R$ be a set. Let $m$ be a function from elements of $x_{5}$ to elements of $M$. Let $n$ be a function from elements of $x_{5}$ to elements of $N$. Then $\operatorname{VanishesTrivially}$ holds for $R$, $m$ and $n$, if there exists a natural number $k$, such that there exists a function $a$ from elements of $x_{5}$ and elements of $\mathrm{Fin}$ applied to $k$ to elements of $R$, such that there exists a function $y$ from elements of $\mathrm{Fin}$ applied to $k$ to elements of $N$, such that for all elements $i$ of $x_{5}$, $\EqtMACRoH {n (i)}{\FinsetSum {\FinsetunivMACRoAC}{j}{(\HSMulhSMulMACRoAL {a (i , j)}{y (j)})}}$ and for all elements $j_{1}$ of $\mathrm{Fin}$ applied to $k$, $\EqtMACRoH {\FinsetSum {\FinsetunivMACRoAC}{i_{1}}{(\HSMulhSMulMACRoAL {a (i_{1} , j_{1})}{m (i_{1})})}}{0}$.

the trace of R and M (from the name)

Let $R$ and $M$ be sets. Then the trace of $R$ and $M$ is a linear map of the set of linear maps of $M$ and $M$ and $R$.

Assume that $1 + f (v)$ is a unit. Then $\operatorname{dilatransvection}$ applied to $h$ is a linear equivalence of $V$ and $V$.

Let $R$ and $V$ be sets. Then $\operatorname{dilatransvections}$ applied to $R$ and $V$ is an element of the power set of the set of linear equivalences of $V$ and $V$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that there exists a dual $f$ of $R$ and $V$, such that there exists an element $v$ of $V$, such that $\operatorname{toLinearMap}$ applied to $e$ is equal to the transvection of $f$ and $v$.

the transvection of h (from the name)

Assume that $\EqtMACRoH {f (v)}{0}$. Then the transvection of $h$ is a linear equivalence of $V$ and $V$.

the transvection of R and V (from the name)

Let $R$ and $V$ be sets. Then the transvection of $R$ and $V$ is an element of the power set of the set of linear equivalences of $V$ and $V$ defined as $\operatorname{ofPred}$ applied to the function that maps $e$ to the proposition that there exists a dual $f$ of $R$ and $V$, such that there exists an element $v$ of $V$, such that there exists an element $\mathrm{hfv}$ of $\EqtMACRoH {f (v)}{0}$, such that $e$ is equal to the transvection of $\mathrm{hfv}$.

the transvection of f and v (from the name)

Let $f$ be a dual of $R$ and $V$. Let $v$ be an element of $V$. Then the transvection of $f$ and $v$ is a linear map of $V$ and $V$.

e is exceptional (from the name)

Let $e$ be a linear equivalence of $V$ and $V$. Then $e$ is exceptional, if $1$ is less than the rank of $K$ and the set of quotients of $V$ and the fixed submodule of $\operatorname{toLinearMap}$ applied to $e$, $\operatorname{fixedReduce} (e)\neq 1$ and there exists an element $a$ of $K$ such that for all quotients $x_{3}$ of $V$ and the fixed submodule of $\operatorname{toLinearMap}$ applied to $e$, $\EqtMACRoH {\operatorname{fixedReduce} (e , x_{3})}{\HSMulhSMulMACRoAL {a}{x_{3}}}$.

v is unimodular (from the name)

Let $R$ be a set. Let $v$ be an element of $M$. Then $v$ is unimodular, if there exists a linear map $f$ of $M$ and $R$, such that $\EqtMACRoH {f (v)}{1}$.

$\operatorname{embeddingGL}$ is a monoid homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{5}})}$ and the set of general linear groups of $x_{2}$ and the set of functions from elements of $n$ to elements of $x_{2}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $A$ to $\operatorname{toGL}$ applied to $A$ and $\mathrm{Matrix\_\_UnitaryGroup\_\_toGL\_one}$ and $\mathrm{Matrix\_\_UnitaryGroup\_\_toGL\_mul}$.

the map star of U (from the name)

Let $U$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{6}})}$. Then the map star of $U$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{5}})}$ defined as the map of $U$ and $\operatorname{star}$.

Let $A$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{6}})}$. Then $\operatorname{toGL}$ applied to $A$ is a general linear group of $x_{2}$ and the set of functions from elements of $n$ to elements of $x_{2}$ defined as the general linear group of the linear equivalence of $A$.

Let $A$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{7}})}$. Then $\operatorname{toLin'}$ applied to $A$ is a linear map of the set of functions from elements of $n$ to elements of $x_{2}$ and the set of functions from elements of $n$ to elements of $x_{2}$ defined as $\operatorname{toLin'}$ applied to $A$.

the linear equivalence of A (from the name)

Let $A$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{7}})}$. Then the linear equivalence of $A$ is a linear equivalence of the set of functions from elements of $n$ to elements of $x_{2}$ and the set of functions from elements of $n$ to elements of $x_{2}$.

the transpose of U (from the docstring)

Let $U$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{6}})}$. Then the transpose of $U$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{unitaryGroup} (n , x_{2})}{x_{5}})}$ defined as the transpose of $U$.

the orthogonal group of n and R (from the name)

Let $n$ and $R$ be sets. Then the orthogonal group of $n$ and $R$ is a submonoid of the set of matrixes of $n$ and $R$ defined as the unitary group of $n$ and $R$.

the special orthogonal group of n and R (from the name)

Let $n$ and $R$ be sets. Then the special orthogonal group of $n$ and $R$ is a submonoid of the set of matrixes of $n$ and $R$ defined as the special unitary group of $n$ and $R$.

the special unitary group of n and x2 (from the name)

Let $n$ and $x_{2}$ be sets. Then the special unitary group of $n$ and $x_{2}$ is a submonoid of the set of matrixes of $n$ and $x_{2}$ defined as the minimum of the unitary group of $n$ and $x_{2}$ and $\operatorname{mker}$ applied to the determinant.

the unitary group of n and x2 (from the name)

Let $n$ and $x_{2}$ be sets. Then the unitary group of $n$ and $x_{2}$ is a submonoid of the set of matrixes of $n$ and $x_{2}$ defined as $\mathrm{unitary}$ applied to the set of matrixes of $n$ and $x_{2}$.

Let $v$ and $w$ be functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $R$. Proof. Let $v$ be arbitrary. Let $w$ be arbitrary. By v. By w. By n. By Matrix__rectVandermonde.

Let $v$ and $w$ be functions from elements of $x_{1}$ to elements of $R$. Let $n$ be a natural number. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $R$. Proof. Let $v$ be arbitrary. Let $w$ be arbitrary. Let $n$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By v. By j1. By Fin__val. By pow. By i1. By w. By j1. By Fin__rev. By Fin__val. By pow. By times. By Matrix__of__app.

Let $v$ be a function from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $R$. Proof. Let $v$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By v. By j1. By Fin__val. By pow. By Matrix__of__app.