Definitions: Mathlib.LinearAlgebra, part 1 of 5

AffineEquiv.arrowCongrdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the arrow congruence of x21 and x22 (from the name)

English

Let $x_{21}$ be an affine equivalence of $x$ and $x_{1}$. Let $x_{22}$ be an affine equivalence of $x_{2}$ and $x_{3}$. Then the arrow congruence of $x_{21}$ and $x_{22}$ is an affine equivalence of the set of affine maps of $x$ and $x_{2}$ and the set of affine maps of $x_{1}$ and $x_{3}$.

AffineEquiv.arrowCongrEquivdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the arrow congruence equivalence of x21 and x22 (from the name)

English

Let $x_{21}$ be an affine equivalence of $x$ and $x_{1}$. Let $x_{22}$ be an affine equivalence of $x_{2}$ and $x_{3}$. Then the arrow congruence equivalence of $x_{21}$ and $x_{22}$ is an equivalence from the set of affine maps of $x$ and $x_{2}$ to the set of affine maps of $x_{1}$ and $x_{3}$.

AffineEquiv.arrowCongrₗdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the arrow congruence of x17 and x18 (from the name)

English

Let $x_{17}$ be an affine equivalence of $x$ and $x_{1}$. Let $x_{18}$ be a linear equivalence of $x_{4}$ and $x_{5}$. Then the arrow congruence of $x_{17}$ and $x_{18}$ is a linear equivalence of the set of affine maps of $x$ and $x_{4}$ and the set of affine maps of $x_{1}$ and $x_{5}$.

AffineEquiv.congrLeftdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the left congruence of e (from the name)

English

Let $R$ and $Q$ be sets. Let $e$ be an affine equivalence of $x$ and $x_{1}$. Then the left congruence of $e$ is an affine equivalence of the set of affine maps of $x$ and $Q$ and the set of affine maps of $x_{1}$ and $Q$.

AffineEquiv.congrLeftₗdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the left congruence of e (from the name)

English

Let $R$ and $W$ be sets. Let $e$ be an affine equivalence of $x$ and $x_{1}$. Then the left congruence of $e$ is a linear equivalence of the set of affine maps of $x$ and $W$ and the set of affine maps of $x_{1}$ and $W$.

AffineEquiv.constVAdddefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the constant sum of v (from the name)

English

Let $k$ and $x$ be sets. Let $v$ be an element of $x_{1}$. Then the constant sum of $v$ is an affine equivalence of $x$ and $x$.

AffineEquiv.constVAddHomdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the constant additive homomorphism of k and x (from the name)

English

Let $k$ and $x$ be sets. Then the constant additive homomorphism of $k$ and $x$ is a monoid homomorphism of the set of multiplicatives of $x_{1}$ and the set of affine equivalences of $x$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $v$ to the constant sum of $\operatorname{toAdd}$ applied to $v$ and $\mathrm{AffineEquiv\_\_constVAdd\_zero}$ applied to $k$ and $x$ and $\mathrm{AffineEquiv\_\_constVAdd\_add}$ applied to $k$ and $x$.

AffineEquiv.constVSubdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the constant difference of k and p (from the name)

English

Let $k$ be a set. Let $p$ be an element of $x$. Then the constant difference of $k$ and $p$ is an affine equivalence of $x$ and $x_{1}$.

AffineEquiv.equivUnitsAffineMapdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the equivalence unit affine map (from the name)

English

The equivalence unit affine map is a multiplicative equivalence of the set of affine equivalences of $x$ and $x$ and the set of units of the set of affine maps of $x$ and $x$.

AffineEquiv.homothetyUnitsMulHomdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the homothety unit multiplicative homomorphism of p (from the name)

English

Let $p$ be an element of $P$. Then the homothety unit multiplicative homomorphism of $p$ is a monoid homomorphism of $\UnitsMACRoAO {R}$ and the set of affine equivalences of $P$ and $P$ defined as the composition of the monoid homomorphism of the inverse of the equivalence unit affine map and the map of the homothety homomorphism of $p$.

AffineEquiv.lineardefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an affine equivalence of $x$ and $x_{1}$. Then $\operatorname{linear}$ applied to $\mathrm{self}$ is a linear equivalence of $x_{2}$ and $x_{3}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

AffineEquiv.linearHomdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the linear homomorphism (from the name)

English

The linear homomorphism is a monoid homomorphism of the set of affine equivalences of $x$ and $x$ and the set of linear equivalences of $x_{1}$ and $x_{1}$.

AffineEquiv.mk'defMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

no wording

English

Let $e$ be a function from elements of $x$ to elements of $x_{1}$. Let $\mathrm{e'}$ be a linear equivalence of $x_{2}$ and $x_{3}$. Let $p$ be an element of $x$ such that for all elements $\mathrm{p'}$ of $x$, $e$ applied to $\mathrm{p'}$ is equal to the sum of $\mathrm{e'}$ applied to the vector difference of $\mathrm{p'}$ and $p$ and $e$ applied to $p$. Then $\operatorname{mk'}$ applied to $e$, $\mathrm{e'}$, $p$ and $h$ is an affine equivalence of $x$ and $x_{1}$.

AffineEquiv.ofBijectivedefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the affine equivalence of h (from the name)

English

Assume that $\operatorname{coe}$ applied to $x_{11}$ is bijective. Then the affine equivalence of $h$ is an affine equivalence of $x$ and $x_{1}$.

AffineEquiv.ofLinearEquivdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the affine equivalence of x4 and x5 (from the name)

English

Let $A$ be a linear equivalence of $V$ and $V$. Let $x_{4}$ and $x_{5}$ be elements of $P$. Then the affine equivalence of $x_{4}$ and $x_{5}$ is an affine equivalence of $P$ and $P$ defined as the composition of the inverse of the vector sum constant of $k$ and $x_{4}$ and the composition of the affine equivalence of $A$ and the vector sum constant of $k$ and $x_{5}$.

AffineEquiv.pointReflectiondefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the point reflection of k and x6 (from the name)

English

Let $k$ be a set. Let $x_{6}$ be an element of $x$. Then the point reflection of $k$ and $x_{6}$ is an affine equivalence of $x$ and $x$ defined as the composition of the constant difference of $k$ and $x_{6}$ and the vector sum constant of $k$ and $x_{6}$.

AffineEquiv.prodAssocdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

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

English

Let $k$, $x$, $x_{1}$ and $x_{2}$ be sets. Then the product associator of $x_{1}$ and $x_{2}$ is an affine equivalence of $\mathrm{Prod}$ applied to $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{2}$.

AffineEquiv.prodCommdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

no wording

English

Let $k$, $x$ and $x_{1}$ be sets. Then $\operatorname{prodComm}$ applied to $k$, $x$ and $x_{1}$ is an affine equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$.

AffineEquiv.prodCongrdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the product congruence of x21 and x22 (from the name)

English

Let $x_{21}$ be an affine equivalence of $x$ and $x_{1}$. Let $x_{22}$ be an affine equivalence of $x_{2}$ and $x_{3}$. Then the product congruence of $x_{21}$ and $x_{22}$ is an affine equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{2}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x_{3}$.

AffineEquiv.refldefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the identity of k and x (from the name)

English

Let $k$ and $x$ be sets. Then the identity of $k$ and $x$ is an affine equivalence of $x$ and $x$.

AffineEquiv.symmdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be an affine equivalence of $x$ and $x_{1}$. Then the inverse of $e$ is an affine equivalence of $x_{1}$ and $x$.

AffineEquiv.toAffineMapdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the affine map of e (from the name)

English

Let $e$ be an affine equivalence of $x$ and $x_{1}$. Then the affine map of $e$ is an affine map of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toEquiv}$ applied to $e$, $\operatorname{toLinearMap}$ applied to $\operatorname{linear}$ applied to $e$ and $\mathrm{AffineEquiv\_\_map\_vadd'}$ applied to $e$.

AffineEquiv.transdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the composition of e and #2 (from the name)

English

Let $e$ be an affine equivalence of $x$ and $x_{1}$. Let $\mathrm{e'}$ be an affine equivalence of $x_{1}$ and $x_{2}$. Then the composition of $e$ and $\mathrm{e'}$ is an affine equivalence of $x$ and $x_{2}$.

AffineEquiv.vaddConstdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the vector sum constant of k and b (from the name)

English

Let $k$ be a set. Let $b$ be an element of $x$. Then the vector sum constant of $k$ and $b$ is an affine equivalence of $x_{1}$ and $x$.

LinearEquiv.toAffineEquivdefMathlib.LinearAlgebra.AffineSpace.AffineEquiv, function or constant

Wording

the affine equivalence of e (from the name)

English

Let $e$ be a linear equivalence of $x$ and $x_{1}$. Then the affine equivalence of $e$ is an affine equivalence of $x$ and $x_{1}$.

Mathlib.LinearAlgebra.AffineSpace.AffineMap

AffineMapstructureMathlib.LinearAlgebra.AffineSpace.AffineMap, type

Wording

affine map of P1 and P2 (from the name)

English

Let $k$, $P_{1}$ and $P_{2}$ be sets. Then the affine maps of $P_{1}$ and $P_{2}$ are a basic type.

AffineMap.compdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an affine map of $P_{2}$ and $P_{3}$. Let $g$ be an affine map of $P_{1}$ and $P_{2}$. Then the composition of $f$ and $g$ is an affine map of $P_{1}$ and $P_{3}$.

AffineMap.constdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the constant of p (from the name)

English

Let $k$ and $P_{1}$ be sets. Let $p$ be an element of $P_{2}$. Then the constant of $p$ is an affine map of $P_{1}$ and $P_{2}$.

AffineMap.fstdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the first component (from the name)

English

The first component is an affine map of $\mathrm{Prod}$ applied to $P_{1}$ and $P_{2}$ and $P_{1}$.

AffineMap.homothetydefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the homothety of c and r (from the name)

English

Let $c$ be an element of $P_{1}$. Let $r$ be an element of $k$. Then the homothety of $c$ and $r$ is an affine map of $P_{1}$ and $P_{1}$ defined as the sum of $\HSMulhSMulMACRoAL {r}{\operatorname{vsub} (\operatorname{id} (k , P_{1}), \operatorname{const} (c))}$ and the constant of $c$.

AffineMap.homothetyAffinedefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the homothety affine of c (from the name)

English

Let $c$ be an element of $P_{1}$. Then the homothety affine of $c$ is an affine map of $k$ and the set of affine maps of $P_{1}$ and $P_{1}$.

AffineMap.homothetyHomdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the homothety homomorphism of c (from the name)

English

Let $c$ be an element of $P_{1}$. Then the homothety homomorphism of $c$ is a monoid homomorphism of $k$ and the set of affine maps of $P_{1}$ and $P_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{homothety}$ applied to $c$ and $\mathrm{AffineMap\_\_homothety\_one}$ applied to $c$ and $\mathrm{AffineMap\_\_homothety\_mul}$ applied to $c$.

AffineMap.iddefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the identity of k and P1 (from the name)

English

Let $k$ and $P_{1}$ be sets. Then the identity of $k$ and $P_{1}$ is an affine map of $P_{1}$ and $P_{1}$.

AffineMap.lineMapdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the line map of x4 and x5 (from the name)

English

Let $x_{4}$ and $x_{5}$ be elements of $P_{1}$. Then the line map of $x_{4}$ and $x_{5}$ is an affine map of $k$ and $P_{1}$ defined as the sum of the affine map of the right scalar multiple of the identity and the vector difference of $x_{5}$ and $x_{4}$ and the constant of $x_{4}$.

AffineMap.lineardefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the linear map between the corresponding vector spaces of self (from the docstring)

English

Let $\mathrm{self}$ be an affine map of $P_{1}$ and $P_{2}$. Then the linear map between the corresponding vector spaces of $\mathrm{self}$ is a linear map of $V_{1}$ and $V_{2}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

AffineMap.linearHomdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the linear homomorphism (from the name)

English

The linear homomorphism is a monoid homomorphism of the set of affine maps of $P_{1}$ and $P_{1}$ and the set of linear maps of $V_{1}$ and $V_{1}$.

AffineMap.mk'defMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $P_{1}$ to elements of $P_{2}$. Let $\mathrm{f'}$ be a linear map of $V_{1}$ and $V_{2}$. Let $p$ be an element of $P_{1}$ such that for all elements $\mathrm{p'}$ of $P_{1}$, $f$ applied to $\mathrm{p'}$ is equal to the sum of $\mathrm{f'}$ applied to the vector difference of $\mathrm{p'}$ and $p$ and $f$ applied to $p$. Then $\operatorname{mk'}$ applied to $f$, $\mathrm{f'}$, $p$ and $h$ is an affine map of $P_{1}$ and $P_{2}$.

AffineMap.pidefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{4}$ to affine maps of $P_{1}$ and $x_{6}$ applied to $i_{1}$. Then the product of $i_{1}$ is an affine map of $P_{1}$ and the set of functions from elements $i$ of $x_{4}$ to elements of $x_{6}$ applied to $i$.

AffineMap.proddefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an affine map of $P_{1}$ and $P_{2}$. Let $g$ be an affine map of $P_{1}$ and $P_{3}$. Then the product of $f$ and $g$ is an affine map of $P_{1}$ and $\mathrm{Prod}$ applied to $P_{2}$ and $P_{3}$.

AffineMap.prodMapdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the product map of f and g (from the name)

English

Let $f$ be an affine map of $P_{1}$ and $P_{2}$. Let $g$ be an affine map of $P_{3}$ and $P_{4}$. Then the product map of $f$ and $g$ is an affine map of $\mathrm{Prod}$ applied to $P_{1}$ and $P_{3}$ and $\mathrm{Prod}$ applied to $P_{2}$ and $P_{4}$.

AffineMap.projdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the projection of i (from the name)

English

Let $i$ be an element of $x_{1}$. Then the projection of $i$ is an affine map of the set of functions from elements $i_{1}$ of $x_{1}$ to elements of $P$ applied to $i_{1}$ and $P$ applied to $i$.

AffineMap.snddefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the second component (from the name)

English

The second component is an affine map of $\mathrm{Prod}$ applied to $P_{1}$ and $P_{2}$ and $P_{2}$.

AffineMap.toConstProdLinearMapdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the constant product linear map of R (from the name)

English

Let $R$ be a set. Then the constant product linear map of $R$ is a linear equivalence of the set of affine maps of $V_{1}$ and $V_{2}$ and $\mathrm{Prod}$ applied to $V_{2}$ and the set of linear maps of $V_{1}$ and $V_{2}$.

AffineMap.toFundefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the underlying function between the affine spaces of self and x7 (from the docstring)

English

Let $\mathrm{self}$ be an affine map of $P_{1}$ and $P_{2}$. Let $x_{7}$ be an element of $P_{1}$. Then the underlying function between the affine spaces of $\mathrm{self}$ and $x_{7}$ is an element of $P_{2}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{7}$.

LinearMap.toAffineMapdefMathlib.LinearAlgebra.AffineSpace.AffineMap, function or constant

Wording

the affine map of f (from the name)

English

Let $f$ be a linear map of $x$ and $x_{1}$. Then the affine map of $f$ is an affine map of $x$ and $x_{1}$.

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

AffineEquiv.ofEqdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the affine equivalence of x6 and x7 (from the name)

English

Let $x_{6}$ and $x_{7}$ be affine subspaces of $k$ and $x_{1}$ such that $\EqtMACRoH {x_{6}}{x_{7}}$. Then the affine equivalence of $x_{6}$ and $x_{7}$ is an affine equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6}}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7}}{x_{9}})}$.

AffineSubspace.ParalleldefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, predicate

Wording

x4 is parallel to x5 (from the name)

English

Let $x_{4}$ and $x_{5}$ be affine subspaces of $k$ and $P$. Then $x_{4}$ is parallel to $x_{5}$, if there exists an element $v$ of $V$, such that $x_{5}$ is equal to the map of the affine map of the constant sum of $v$ and $x_{4}$.

AffineSubspace.comapdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the preimage of f and s (from the docstring)

English

Let $f$ be an affine map of $x_{1}$ and $x_{3}$. Let $s$ be an affine subspace of $k$ and $x_{3}$. Then the preimage of $f$ and $s$ is an affine subspace of $k$ and $x_{1}$.

AffineSubspace.gciMapComapdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

no wording

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then $\operatorname{gciMapComap}$ applied to $\mathrm{hf}$ is a Galois coinsertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

AffineSubspace.inclusiondefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the inclusion of h1 (from the name)

English

Assume that $x_{6} \leq x_{7}$. Then the inclusion of $h_{1}$ is an affine map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6}}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7}}{x_{9}})}$.

AffineSubspace.mapdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the map of f and s (from the name)

English

Let $f$ be an affine map of $x_{1}$ and $x_{3}$. Let $s$ be an affine subspace of $k$ and $x_{1}$. Then the map of $f$ and $s$ is an affine subspace of $k$ and $x_{3}$.

AffineSubspace.proddefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the product of s and t (from the name)

English

Let $s$ be an affine subspace of $k$ and $P$. Let $t$ be an affine subspace of $k$ and $Q$. Then the product of $s$ and $t$ is an affine subspace of $k$ and $\mathrm{Prod}$ applied to $P$ and $Q$.

AffineSubspace.subtypedefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the subtype of s (from the name)

English

Let $s$ be an affine subspace of $k$ and $P$. Then the subtype of $s$ is an affine map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$ and $P$.

AffineSubspace.topEquivdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic, function or constant

Wording

the top equivalence of V and P (from the name)

English

Let $k$, $V$ and $P$ be sets. Then the top equivalence of $V$ and $P$ is an affine equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $P$.

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

AffineSubspacestructureMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, type

Wording

affine subspace of k and P (from the name)

English

Let $k$ and $P$ be sets. Then the affine subspaces of $k$ and $P$ are a basic type.

AffineSubspace.carrierdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the carrier of self (from the name)

English

Let $\mathrm{self}$ be an affine subspace of $k$ and $P$. Then the carrier of $\mathrm{self}$ is an element of $\wp P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

AffineSubspace.directiondefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the direction of s (from the docstring)

English

Let $s$ be an affine subspace of $k$ and $P$. Then the direction of $s$ is a submodule of $k$ and $V$ defined as the vector span of $k$ and $s$.

AffineSubspace.directionOfNonemptydefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the direction of h (from the name)

English

Assume that $s$ is nonempty. Then the direction of $h$ is a submodule of $k$ and $V$.

AffineSubspace.gidefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

no wording

English

Let $k$, $V$ and $P$ be sets. Then $\operatorname{gi}$ applied to $k$, $V$ and $P$ is a Galois insertion of $\mathrm{affineSpan}$ applied to $k$ and $\operatorname{instSetLike}$.

AffineSubspace.mk'defMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

no wording

English

Let $p$ be an element of $P$. Let $\mathrm{direction}$ be a submodule of $k$ and $V$. Then $\operatorname{mk'}$ applied to $p$ and $\mathrm{direction}$ is an affine subspace of $k$ and $P$.

Submodule.ofAffineSubspacedefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the submodule of p and hp (from the name)

English

Let $p$ be an affine subspace of $k$ and $V$ such that $0$ is an element of $p$. Then the submodule of $p$ and $\mathrm{hp}$ is a submodule of $k$ and $V$.

Submodule.toAffineSubspacedefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the affine subspace of p (from the name)

English

Let $p$ be a submodule of $k$ and $V$. Then the affine subspace of $p$ is an affine subspace of $k$ and $V$.

affineSpandefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the affine span of k and s (from the docstring)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then the affine span of $k$ and $s$ is an affine subspace of $k$ and $P$.

spanPointsdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the span point of k and s (from the name)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then the span point of $k$ and $s$ is an element of $\wp P$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that there exists an element $x_{4}$ of $P$, such that $x_{4}$ is an element of $s$ and there exists an element $v$ of $V$ such that $v$ is an element of the vector span of $k$ and $s$ and $p$ is equal to the sum of $v$ and $x_{4}$.

vectorSpandefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs, function or constant

Wording

the vector span of k and s (from the name)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then the vector span of $k$ and $s$ is a submodule of $k$ and $V$ defined as the span of $k$ and the vector difference of $s$ and $s$.

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range

AffineMap.rangedefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be an affine map of $x_{2}$ and $x_{3}$. Then the range of $f$ is an affine subspace of $R$ and $x_{3}$.

AffineMap.rangeRestrictdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Range, function or constant

Wording

no wording

English

Let $f$ be an affine map of $x_{2}$ and $x_{3}$. Then $\operatorname{rangeRestrict}$ applied to $f$ is an affine map of $x_{2}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{11}})}$.

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift

AffineSubspace.shiftdefMathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift, function or constant

Wording

the shift of c and r (from the name)

English

Let $s$ be an affine subspace of $k$ and $P$. Let $c$ be an element of $P$. Let $r$ be an element of $k$. Then the shift of $c$ and $r$ is an affine subspace of $k$ and $P$ defined as $\mathrm{dite}$ applied to $\mathrm{Nonempty}$ applied to $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {s}{x_{4}})}$, the function that maps $h$ to the map of the affine map of the constant sum of $\HSMulhSMulMACRoAL {(1 - r)}{\operatorname{vsub} (c , \operatorname{some} (h))}$ and $s$ and the function that maps $h_{1}$ to the bottom.

Mathlib.LinearAlgebra.AffineSpace.Basis

AffineBasisstructureMathlib.LinearAlgebra.AffineSpace.Basis, type

Wording

affine basis of k and P (from the name)

English

Let $x$, $k$ and $P$ be sets. Then the affine bases of $k$ and $P$ are a basic type.

AffineBasis.basisOfdefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

the basis of b and i (from the name)

English

Let $b$ be an affine basis of $k$ and $P$. Let $i$ be an element of $x$. Then the basis of $b$ and $i$ is a basis of $k$ and $V$.

AffineBasis.coorddefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

the coordinate of b and i (from the name)

English

Let $b$ be an affine basis of $k$ and $P$. Let $i$ be an element of $x$. Then the coordinate of $b$ and $i$ is an affine map of $P$ and $k$.

AffineBasis.coordsdefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

no wording

English

Let $b$ be an affine basis of $k$ and $P$. Then $\operatorname{coords}$ applied to $b$ is an affine map of $P$ and the set of functions from elements of $x$ to elements of $k$.

AffineBasis.reindexdefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

the reindexing of b and e (from the name)

English

Let $b$ be an affine basis of $k$ and $P$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $b$ and $e$ is an affine basis of $k$ and $P$.

AffineBasis.toFundefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

the affine basis of self and x5 (from the name)

English

Let $\mathrm{self}$ be an affine basis of $k$ and $P$. Let $x_{5}$ be an element of $x$. Then the affine basis of $\mathrm{self}$ and $x_{5}$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{5}$.

finsuppAffineCoordsdefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

no wording

English

Let $x$ and $k$ be sets. Then $\mathrm{finsuppAffineCoords}$ applied to $x$ and $k$ is an affine subspace of $k$ and $\FinsuppMACRoQ {x}{k}$ defined as the preimage of the affine map of the linear combination of $k$ and $1$ and the affine span of $k$ and $\operatorname{singleton}$ applied to $1$.

fintypeAffineCoordsdefMathlib.LinearAlgebra.AffineSpace.Basis, function or constant

Wording

no wording

English

Let $x$ and $k$ be sets. Then $\mathrm{fintypeAffineCoords}$ applied to $x$ and $k$ is an affine subspace of $k$ and the set of functions from elements of $x$ to elements of $k$ defined as the preimage of the affine map of the linear combination of $k$ and $1$ and the affine span of $k$ and $\operatorname{singleton}$ applied to $1$.

Mathlib.LinearAlgebra.AffineSpace.Centroid

Finset.centroiddefMathlib.LinearAlgebra.AffineSpace.Centroid, function or constant

Wording

the centroid of s and p (from the name)

English

Let $k$ be a set. Let $s$ be a finite set of $x_{4}$. Let $p$ be a function from elements of $x_{4}$ to elements of $P$. Then the centroid of $s$ and $p$ is an element of $P$ defined as $\operatorname{affineCombination}$ applied to $k$, $s$, $p$ and $\operatorname{centroidWeights}$ applied to $k$ and $s$.

Finset.centroidWeightsdefMathlib.LinearAlgebra.AffineSpace.Centroid, function or constant

Wording

no wording

English

Let $k$ be a set. Let $s$ be a finite set of $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{centroidWeights}$ applied to $k$, $s$ and $x_{2}$ is an element of $k$ defined as $\operatorname{const}$ applied to $x_{1}$, $\operatorname{inv}$ applied to the cardinality of $s$ and $x_{2}$.

Finset.centroidWeightsIndicatordefMathlib.LinearAlgebra.AffineSpace.Centroid, function or constant

Wording

no wording

English

Let $k$ be a set. Let $s$ be a finite set of $x_{1}$. Let $x_{2}$ be an element of $x_{1}$. Then $\operatorname{centroidWeightsIndicator}$ applied to $k$, $s$ and $x_{2}$ is an element of $k$ defined as the indicator of $\operatorname{centroidWeights}$ applied to $k$ and $s$ and $x_{2}$.

Mathlib.LinearAlgebra.AffineSpace.Combination

AffineMap.weightedVSubOfPointdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

the weighted difference of s and w (from the name)

English

Let $P$ be a set. Let $s$ be a finite set of $x_{4}$. Let $w$ be a function from elements of $x_{4}$ to elements of $k$. Then the weighted difference of $s$ and $w$ is an affine map of $\mathrm{Prod}$ applied to the set of functions from elements of $x_{4}$ to elements of $P$ and $P$ and $V$.

Finset.affineCombinationdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

the affine combination of s and p (from the name)

English

Let $k$ be a set. Let $s$ be a finite set of $x_{3}$. Let $p$ be a function from elements of $x_{3}$ to elements of $P$. Then the affine combination of $s$ and $p$ is an affine map of the set of functions from elements of $x_{3}$ to elements of $k$ and $P$.

Finset.affineCombinationLineMapWeightsdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

no wording

English

Let $i$, $j$ and $x_{3}$ be elements of $x_{1}$. Let $c$ be an element of $k$. Then $\operatorname{affineCombinationLineMapWeights}$ applied to $i$, $j$, $c$ and $x_{3}$ is an element of $k$ defined as $\mathrm{plus} (\HSMulhSMulMACRoAL {c}{\operatorname{weightedVSubVSubWeights} (k , j , i)}, \operatorname{single} (i , 1), x_{3})$.

Finset.weightedVSubdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

the weighted difference of s and p (from the name)

English

Let $s$ be a finite set of $x_{3}$. Let $p$ be a function from elements of $x_{3}$ to elements of $P$. Then the weighted difference of $s$ and $p$ is a linear map of the set of functions from elements of $x_{3}$ to elements of $k$ and $V$.

Finset.weightedVSubOfPointdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

the weighted difference of p and b (from the name)

English

Let $s$ be a finite set of $x_{3}$. Let $p$ be a function from elements of $x_{3}$ to elements of $P$. Let $b$ be an element of $P$. Then the weighted difference of $p$ and $b$ is a linear map of the set of functions from elements of $x_{3}$ to elements of $k$ and $V$ defined as $\FinsetSum {s}{i}{\operatorname{smulRight} (\operatorname{proj} (i), \operatorname{vsub} (p (i), b))}$.

Finset.weightedVSubVSubWeightsdefMathlib.LinearAlgebra.AffineSpace.Combination, function or constant

Wording

no wording

English

Let $k$ be a set. Let $i$, $j$ and $x_{3}$ be elements of $x_{1}$. Then $\operatorname{weightedVSubVSubWeights}$ applied to $k$, $i$, $j$ and $x_{3}$ is an element of $k$ defined as $\mathrm{minus} (\operatorname{single} (i , 1), \operatorname{single} (j , 1), x_{3})$.

Mathlib.LinearAlgebra.AffineSpace.Dimension

AffineSubspace.dimdefMathlib.LinearAlgebra.AffineSpace.Dimension, function or constant

Wording

the dimension of s (from the docstring)

English

Let $s$ be an affine subspace of $R$ and $A$. Then the dimension of $s$ is an element of $\mathrm{WithBot}$ applied to the set of cardinals defined as $\iteMACRoG {(\EqtMACRoH {s}{\operatorname{bot}})}{\operatorname{bot}}{\operatorname{some} (\operatorname{rank} (R , \SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{direction} (s)}{x_{4}})}))}$.

AffineSubspace.finDimdefMathlib.LinearAlgebra.AffineSpace.Dimension, function or constant

Wording

the dimension of s (from the docstring)

English

Let $s$ be an affine subspace of $R$ and $A$. Then the dimension of $s$ is an element of $\mathrm{WithBot}$ applied to $\Natural$ defined as the map of $\operatorname{coe}$ applied to the natural number and the dimension of $s$.

Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

CollineardefMathlib.LinearAlgebra.AffineSpace.FiniteDimensional, predicate

Wording

k is collinear (from the docstring)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then $k$ is collinear, if $\operatorname{rank} (k , \SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{vectorSpan} (k , s)}{x_{4}})})\leq 1$.

CoplanardefMathlib.LinearAlgebra.AffineSpace.FiniteDimensional, predicate

Wording

k is coplanar (from the docstring)

English

Let $k$ be a set. Let $s$ be an element of $\wp P$. Then $k$ is coplanar, if $\operatorname{rank} (k , \SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{vectorSpan} (k , s)}{x_{4}})})\leq 2$.

Mathlib.LinearAlgebra.AffineSpace.Homogenization

HomogenizationdefMathlib.LinearAlgebra.AffineSpace.Homogenization, type

Wording

homogenization of R and P (from the name)

English

Let $R$ and $P$ be sets. Then a homogenization of $R$ and $P$ is an element of the function that maps $R$ and $P$ to $\mathrm{Prod}$ applied to $V$ and $R$.

Homogenization.congrdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the congruence of f (from the name)

English

Let $f$ be an affine equivalence of $x_{2}$ and $x_{7}$. Then the congruence of $f$ is a linear equivalence of the set of homogenizations of $R$ and $x_{2}$ and the set of homogenizations of $R$ and $x_{7}$.

Homogenization.liftdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the lift (from the name)

English

The lift is an additive equivalence of the set of affine maps of $P$ and $W$ and the set of linear maps of the set of homogenizations of $R$ and $P$ and $W$.

Homogenization.liftₗdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the lift of S (from the name)

English

Let $S$ be a set. Then the lift of $S$ is a linear equivalence of the set of affine maps of $P$ and $W$ and the set of linear maps of the set of homogenizations of $R$ and $P$ and $W$ defined as the linear equivalence of the lift and the function that maps $x_{8}$ and $x_{9}$ to $\mathrm{Homogenization\_\_lift\_smul}$ applied to $x_{8}$ and $x_{9}$.

Homogenization.mapdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the map of f (from the name)

English

Let $f$ be an affine map of $x_{2}$ and $x_{7}$. Then the map of $f$ is a linear map of the set of homogenizations of $R$ and $x_{2}$ and the set of homogenizations of $R$ and $x_{7}$ defined as $\operatorname{lift}$ applied to the composition of the embedding of the affine space into the homogenization and $f$.

Homogenization.ofPointdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the embedding of the affine space into the homogenization (from the docstring)

English

The embedding of the affine space into the homogenization is an affine map of $P$ and the set of homogenizations of $R$ and $P$ defined as the product of the affine map of the inverse of the vector sum constant of $R$ and $\operatorname{arbitrary}$ applied to $P$ and the constant of $1$.

Homogenization.ofVectordefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the embedding of the vector space into the homogenization (from the docstring)

English

The embedding of the vector space into the homogenization is a linear map of $V$ and the set of homogenizations of $R$ and $P$ defined as the linear map between the corresponding vector spaces of the embedding of the affine space into the homogenization.

Homogenization.toProddefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

the product (from the name)

English

The product is a linear equivalence of the set of homogenizations of $R$ and $V$ and $\mathrm{Prod}$ applied to $V$ and $R$.

Homogenization.weightdefMathlib.LinearAlgebra.AffineSpace.Homogenization, function or constant

Wording

no wording

English

$\operatorname{weight}$ is a linear map of the set of homogenizations of $R$ and $P$ and $R$ defined as $\operatorname{lift}$ applied to the constant of $1$.

Mathlib.LinearAlgebra.AffineSpace.Independent

AffineIndepOndefMathlib.LinearAlgebra.AffineSpace.Independent, predicate

Wording

no wording

English

Let $k$ be a set. Let $p$ be a function from elements of $x_{4}$ to elements of $P$. Let $s$ be an element of $\wp x_{4}$. Then $\mathrm{AffineIndepOn}$ holds for $k$, $p$ and $s$, if $\mathrm{AffineIndependent}$ holds for $k$ and the function that maps $x_{5}$ to $p$ applied to $x_{5}$.

AffineIndependentdefMathlib.LinearAlgebra.AffineSpace.Independent, predicate

Wording

no wording

English

Let $k$ be a set. Let $p$ be a function from elements of $x_{4}$ to elements of $P$. Then $\mathrm{AffineIndependent}$ holds for $k$ and $p$, if for all finite sets $s$ of $x_{4}$, for all functions $w$ from elements of $x_{4}$ to elements of $k$, if $\EqtMACRoH {\FinsetSum {s}{i_{1}}{w (i_{1})}}{0}$, then if $\EqtMACRoH {\operatorname{weightedVSub} (s , p , w)}{0}$, then for all elements $i$ of $x_{4}$, if $i$ is an element of $s$, then $\EqtMACRoH {w (i)}{0}$.

Mathlib.LinearAlgebra.AffineSpace.Matrix

AffineBasis.toMatrixdefMathlib.LinearAlgebra.AffineSpace.Matrix, function or constant

Wording

the matrix of b and q (from the name)

English

Let $b$ be an affine basis of $k$ and $P$. Let $q$ be a function from elements of $x_{5}$ to elements of $P$. Then the matrix of $b$ and $q$ is a matrix of $x$ and $k$ defined as the function that maps $i$ and $j$ to $\operatorname{coord}$ applied to $b$, $j$ and $q$ applied to $i$.

Mathlib.LinearAlgebra.AffineSpace.Midpoint

AddMonoidHom.ofMapMidpointdefMathlib.LinearAlgebra.AffineSpace.Midpoint, function or constant

Wording

the additive monoid homomorphism of h0 (from the name)

English

Let $R$ and $\mathrm{R'}$ be sets. Let $f$ be a function from elements of $E$ to elements of $F$ such that $\EqtMACRoH {f (0)}{0}$ and for all elements $x_{8}$ of $E$, for all elements $y$ of $E$, $f$ applied to the midpoint of $x_{8}$ and $y$ is equal to the midpoint of $f$ applied to $x_{8}$ and $f$ applied to $y$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $E$ and $F$.

midpointdefMathlib.LinearAlgebra.AffineSpace.Midpoint, function or constant

Wording

the midpoint of x5 and y (from the name)

English

Let $R$ be a set. Let $x_{5}$ and $y$ be elements of $P$. Then the midpoint of $x_{5}$ and $y$ is an element of $P$ defined as $\operatorname{lineMap}$ applied to $x_{5}$, $y$ and the inverse of $2$.

Mathlib.LinearAlgebra.AffineSpace.Restrict

AffineEquiv.affineSubspaceMapdefMathlib.LinearAlgebra.AffineSpace.Restrict, function or constant

Wording

the affine subspace map of e and s (from the name)

English

Let $e$ be an affine equivalence of $x_{1}$ and $x_{3}$. Let $s$ be an affine subspace of $k$ and $x_{1}$. Then the affine subspace map of $e$ and $s$ is an affine equivalence of $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {s}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toAffineMap} (e), s)}{x_{12}})}$.

AffineMap.restrictdefMathlib.LinearAlgebra.AffineSpace.Restrict, function or constant

Wording

no wording

English

Let $x_{11}$ be an affine map of $x_{1}$ and $x_{3}$ such that the map of $x_{11}$ and $E$ is less than or equal to $F$. Then $\operatorname{restrict}$ applied to $x_{11}$ and $\mathrm{hEF}$ is an affine map of $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {E}{x_{12}})}$ and $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {F}{x_{13}})}$.

Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Affine.SimplexstructureMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, type

Wording

simplex of P and n (from the name)

English

Let $k$ and $P$ be sets. Let $n$ be a natural number. Then the simplexes of $P$ and $n$ are a basic type.

Affine.Simplex.closedInteriordefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the closed interior of s (from the name)

English

Let $s$ be a simplex of $P$ and $n$. Then the closed interior of $s$ is an element of $\wp P$ defined as the interior of $\SetIccMACRoP {0}{1}$ and $s$.

Affine.Simplex.facedefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the face of s and h (from the name)

English

Let $s$ be a simplex of $P$ and $n$. Assume that $\FinsetcardMACRoM {\mathrm{fs}}= m + 1$. Then the face of $s$ and $h$ is a simplex of $P$ and $m$.

Affine.Simplex.faceOppositedefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the face of s and i (from the docstring)

English

Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the face of $s$ and $i$ is a simplex of $P$ and $n - 1$.

Affine.Simplex.interiordefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the interior of s (from the docstring)

English

Let $s$ be a simplex of $P$ and $n$. Then the interior of $s$ is an element of $\wp P$ defined as the interior of the open interval of $0$ and $1$ and $s$.

Affine.Simplex.mapdefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the map of s and f (from the name)

English

Let $s$ be a simplex of $P$ and $n$. Let $f$ be an affine map of $P$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the map of $s$ and $f$ is a simplex of $x_{1}$ and $n$.

Affine.Simplex.mkOfPointdefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

no wording

English

Let $k$ be a set. Let $p$ be an element of $P$. Then $\operatorname{mkOfPoint}$ applied to $k$ and $p$ is a simplex of $P$ and $0$.

Affine.Simplex.pointsdefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the point of self and x4 (from the name)

English

Let $\mathrm{self}$ be a simplex of $P$ and $n$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the point of $\mathrm{self}$ and $x_{4}$ is an element of $P$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{4}$.

Affine.Simplex.reindexdefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the reindexing of s and e (from the name)

English

Let $s$ be a simplex of $P$ and $m$. Let $e$ be an element of $\EquivMACRoAE {\mathrm{Fin} (m + 1)}{\mathrm{Fin} (n + 1)}$. Then the reindexing of $s$ and $e$ is a simplex of $P$ and $n$.

Affine.Simplex.restrictdefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

no wording

English

Let $s$ be a simplex of $P$ and $n$. Let $S$ be an affine subspace of $k$ and $P$ such that the affine span of $k$ and the range of $\operatorname{points}$ applied to $s$ is less than or equal to $S$. Then $\operatorname{restrict}$ applied to $s$, $S$ and $\mathrm{hS}$ is a simplex of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$ and $n$.

Affine.Simplex.setInteriordefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, function or constant

Wording

the interior of I and s (from the docstring)

English

Let $I$ be an element of $\wp k$. Let $s$ be a simplex of $P$ and $n$. Then the interior of $I$ and $s$ is an element of $\wp P$ defined as $\operatorname{ofPred}$ applied to the function that maps $p$ to the proposition that there exists a function $w$ from elements of $\mathrm{Fin}$ applied to $n + 1$ to elements of $k$, such that $\EqtMACRoH {\FinsetSum {\FinsetunivMACRoAC}{i}{w (i)}}{1}$, for all elements $i_{1}$ of $\mathrm{Fin}$ applied to $n + 1$, $\MembershipmemMACRoT {I}{w (i_{1})}$ and $\operatorname{affineCombination}$ applied to $k$, the universal set, $\operatorname{points}$ applied to $s$ and $w$ is equal to $p$.

Affine.TriangledefMathlib.LinearAlgebra.AffineSpace.Simplex.Basic, type

Wording

triangle of k and P (from the name)

English

Let $k$ and $P$ be sets. Then a triangle of $k$ and $P$ is an element of the function that maps $k$ and $P$ to the set of simplexes of $P$ and $2$.

Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Affine.Simplex.centroiddefMathlib.LinearAlgebra.AffineSpace.Simplex.Centroid, function or constant

Wording

the centroid of t (from the docstring)

English

Let $t$ be a simplex of $P$ and $n$. Then the centroid of $t$ is an element of $P$ defined as the centroid of the universal set and $\operatorname{points}$ applied to $t$.

Affine.Simplex.faceOppositeCentroiddefMathlib.LinearAlgebra.AffineSpace.Simplex.Centroid, function or constant

Wording

the face opposite centroid of s and i (from the name)

English

Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the face opposite centroid of $s$ and $i$ is an element of $P$ defined as the centroid of the face of $s$ and $i$.

Affine.Simplex.medialdefMathlib.LinearAlgebra.AffineSpace.Simplex.Centroid, function or constant

Wording

no wording

English

Let $s$ be a simplex of $P$ and $n$. Then $\operatorname{medial}$ applied to $s$ is a simplex of $P$ and $n$.

Affine.Simplex.mediandefMathlib.LinearAlgebra.AffineSpace.Simplex.Centroid, function or constant

Wording

the median of s and i (from the docstring)

English

Let $s$ be a simplex of $P$ and $n$. Let $i$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the median of $s$ and $i$ is an affine subspace of $k$ and $P$ defined as the affine span of $k$ and $\operatorname{insert}$ applied to the point of $s$ and $i$ and $\operatorname{singleton}$ applied to the face opposite centroid of $s$ and $i$.

Mathlib.LinearAlgebra.AffineSpace.Slope

slopedefMathlib.LinearAlgebra.AffineSpace.Slope, function or constant

Wording

the slope of a and b (from the name)

English

Let $f$ be a function from elements of $k$ to elements of $\mathrm{PE}$. Let $a$ and $b$ be elements of $k$. Then the slope of $a$ and $b$ is an element of $E$ defined as $\HSMulhSMulMACRoAL {\operatorname{inv} (b - a)}{\operatorname{vsub} (f (b), f (a))}$.

Mathlib.LinearAlgebra.Alternating.Basic

AlternatingMapstructureMathlib.LinearAlgebra.Alternating.Basic, type

Wording

alternating map of N and x5 (from the name)

English

Let $R$, $M$, $N$ and $x_{5}$ be sets. Then the alternating maps of $N$ and $x_{5}$ are a basic type.

AlternatingMap.codRestrictdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

no wording

English

Let $f$ be an alternating map of $N$ and $x_{5}$. Let $p$ be a submodule of $R$ and $N$ such that for all functions $v$ from elements of $x_{5}$ to elements of $M$, $\MembershipmemMACRoT {p}{f (v)}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $h$ is an alternating map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $x_{5}$.

AlternatingMap.compLinearMapdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the composition linear map of f and g (from the name)

English

Let $f$ be an alternating map of $N$ and $x_{5}$. Let $g$ be a linear map of $x_{6}$ and $M$. Then the composition linear map of $f$ and $g$ is an alternating map of $N$ and $x_{5}$.

AlternatingMap.constLinearEquivOfIsEmptydefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the constant linear equivalence (from the name)

English

The constant linear equivalence is a linear equivalence of $\mathrm{N''}$ and the set of alternating maps of $\mathrm{N''}$ and $x$.

AlternatingMap.constOfIsEmptydefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the constant of m (from the name)

English

Let $R$, $M$ and $x_{5}$ be sets. Let $m$ be an element of $N$. Then the constant of $m$ is an alternating map of $N$ and $x_{5}$.

AlternatingMap.domDomCongrdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the domain domain congruence of x7 and f (from the name)

English

Let $x_{7}$ be an equivalence from $x_{5}$ to $x_{6}$. Let $f$ be an alternating map of $N$ and $x_{5}$. Then the domain domain congruence of $x_{7}$ and $f$ is an alternating map of $N$ and $x_{6}$.

AlternatingMap.domDomCongrEquivdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the domain domain congruence equivalence of x7 (from the name)

English

Let $x_{7}$ be an equivalence from $x_{5}$ to $x_{6}$. Then the domain domain congruence equivalence of $x_{7}$ is an additive equivalence of the set of alternating maps of $N$ and $x_{5}$ and the set of alternating maps of $N$ and $x_{6}$.

AlternatingMap.domDomCongrₗdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the domain domain congruence of S and x9 (from the name)

English

Let $S$ be a set. Let $x_{9}$ be an equivalence from $x_{5}$ to $x_{6}$. Then the domain domain congruence of $S$ and $x_{9}$ is a linear equivalence of the set of alternating maps of $N$ and $x_{5}$ and the set of alternating maps of $N$ and $x_{6}$.

AlternatingMap.domLCongrdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the domain congruence of e (from the name)

English

Let $R$, $N$, $x_{5}$ and $S$ be sets. Let $e$ be a linear equivalence of $M$ and $x_{6}$. Then the domain congruence of $e$ is a linear equivalence of the set of alternating maps of $N$ and $x_{5}$ and the set of alternating maps of $N$ and $x_{5}$.

AlternatingMap.ofSubsingletondefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the alternating map of i (from the name)

English

Let $R$, $M$ and $N$ be sets. Let $i$ be an element of $x_{5}$. Then the alternating map of $i$ is an equivalence from the set of linear maps of $M$ and $N$ to the set of alternating maps of $N$ and $x_{5}$.

AlternatingMap.pidefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x_{4}$ to alternating maps of $N$ applied to $i_{1}$ and $x_{3}$. Then the product of $i_{1}$ is an alternating map of the set of functions from elements $i$ of $x_{4}$ to elements of $N$ applied to $i$ and $x_{3}$.

AlternatingMap.proddefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be an alternating map of $N$ and $x_{7}$. Let $g$ be an alternating map of $P$ and $x_{7}$. Then the product of $f$ and $g$ is an alternating map of $\mathrm{Prod}$ applied to $N$ and $P$ and $x_{7}$.

AlternatingMap.smulRightdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the right scalar multiple of f and z (from the name)

English

Let $f$ be an alternating map of $R$ and $x_{2}$. Let $z$ be an element of $x_{1}$. Then the right scalar multiple of $f$ and $z$ is an alternating map of $x_{1}$ and $x_{2}$.

AlternatingMap.toMultilinearMapLMdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

no wording

English

$\operatorname{toMultilinearMapLM}$ is a linear map of the set of alternating maps of $N$ and $x_{5}$ and the set of multilinear maps of the function that maps $x_{8}$ to $M$ and $N$.

LinearEquiv.alternatingMapCongrRightdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the right alternating map congruence of e (from the name)

English

Let $e$ be a linear equivalence of $\mathrm{N''}$ and $x_{1}$. Then the right alternating map congruence of $e$ is a linear equivalence of the set of alternating maps of $\mathrm{N''}$ and $x$ and the set of alternating maps of $x_{1}$ and $x$.

LinearMap.compAlternatingMapdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the composition alternating map of g and f (from the name)

English

Let $g$ be a linear map of $N$ and $x_{6}$. Let $f$ be an alternating map of $N$ and $x_{5}$. Then the composition alternating map of $g$ and $f$ is an alternating map of $x_{6}$ and $x_{5}$.

LinearMap.compAlternatingMapₗdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

the composition alternating map of S and g (from the name)

English

Let $S$ be a set. Let $g$ be a linear map of $N$ and $x_{6}$. Then the composition alternating map of $S$ and $g$ is a linear map of the set of alternating maps of $N$ and $x_{5}$ and the set of alternating maps of $x_{6}$ and $x_{5}$.

MultilinearMap.alternatizationdefMathlib.LinearAlgebra.Alternating.Basic, function or constant

Wording

no wording

English

$\operatorname{alternatization}$ is an additive monoid homomorphism of the set of multilinear maps of the function that maps $x_{8}$ to $M$ and $\mathrm{N'}$ and the set of alternating maps of $\mathrm{N'}$ and $x_{5}$.

Mathlib.LinearAlgebra.Alternating.Curry

AlternatingMap.curryLeftdefMathlib.LinearAlgebra.Alternating.Curry, function or constant

Wording

the left curry of f (from the name)

English

Let $f$ be an alternating map of $N$ and $\mathrm{Fin}$ applied to the successor of $n$. Then the left curry of $f$ is a linear map of $M$ and the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n$.

AlternatingMap.curryLeftLinearMapdefMathlib.LinearAlgebra.Alternating.Curry, function or constant

Wording

the curry left linear map (from the name)

English

The curry left linear map is a linear map of the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to the successor of $n$ and the set of linear maps of $M$ and the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to the function that maps $f$ to the left curry of $f$ and $\mathrm{AlternatingMap\_\_curryLeft\_add}$ and $\mathrm{AlternatingMap\_\_curryLeft\_smul}$.

Mathlib.LinearAlgebra.Alternating.DomCoprod

AlternatingMap.domCoproddefMathlib.LinearAlgebra.Alternating.DomCoprod, function or constant

Wording

the domain coproduct of a and b (from the name)

English

Let $a$ be an alternating map of $x_{5}$ and $x$. Let $b$ be an alternating map of $x_{6}$ and $x_{1}$. Then the domain coproduct of $a$ and $b$ is an alternating map of the set of tensor products of $x_{5}$ and $x_{6}$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

AlternatingMap.domCoprod'defMathlib.LinearAlgebra.Alternating.DomCoprod, function or constant

Wording

the domain coproduct (from the name)

English

The domain coproduct is a linear map of the set of tensor products of the set of alternating maps of $x_{5}$ and $x$ and the set of alternating maps of $x_{6}$ and $x_{1}$ and the set of alternating maps of the set of tensor products of $x_{5}$ and $x_{6}$ and $\mathrm{Sum}$ applied to $x$ and $x_{1}$.

AlternatingMap.domCoprod.summanddefMathlib.LinearAlgebra.Alternating.DomCoprod, function or constant

Wording

the summand of b and x16 (from the name)

English

Let $a$ be an alternating map of $x_{5}$ and $x$. Let $b$ be an alternating map of $x_{6}$ and $x_{1}$. Let $x_{16}$ be an element of $\operatorname{ModSumCongr}$ applied to $x$ and $x_{1}$. Then the summand of $b$ and $x_{16}$ is a multilinear map of the function that maps $x_{17}$ to $x_{4}$ and the set of tensor products of $x_{5}$ and $x_{6}$.

Equiv.Perm.ModSumCongrdefMathlib.LinearAlgebra.Alternating.DomCoprod, type

Wording

no wording

English

Let $x$ and $x_{1}$ be sets. Then an element of $\operatorname{ModSumCongr}$ applied to $x$ and $x_{1}$ is an element of the function that maps $x$ and $x_{1}$ to the set of quotients of the set of permutations of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ and the range of the sum congruence homomorphism of $x$ and $x_{1}$.

Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

AlternatingMap.alternatizeUncurryFindefMathlib.LinearAlgebra.Alternating.Uncurry.Fin, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n$. Then $\operatorname{alternatizeUncurryFin}$ applied to $f$ is an alternating map of $N$ and $\mathrm{Fin}$ applied to $n + 1$.

AlternatingMap.alternatizeUncurryFinLMdefMathlib.LinearAlgebra.Alternating.Uncurry.Fin, function or constant

Wording

no wording

English

$\operatorname{alternatizeUncurryFinLM}$ is a linear map of the set of linear maps of $M$ and the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n$ and the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n + 1$.

Mathlib.LinearAlgebra.AnnihilatingPolynomial

Polynomial.annIdealdefMathlib.LinearAlgebra.AnnihilatingPolynomial, function or constant

Wording

no wording

English

Let $R$ be a set. Let $a$ be an element of $A$. Then $\operatorname{annIdeal}$ applied to $R$ and $a$ is an ideal of the set of polynomials of $R$ defined as the kernel of $\operatorname{toRingHom}$ applied to the algebra evaluation of $a$.

Polynomial.annIdealGeneratordefMathlib.LinearAlgebra.AnnihilatingPolynomial, function or constant

Wording

no wording

English

Let $x$ be a set. Let $a$ be an element of $A$. Then $\operatorname{annIdealGenerator}$ applied to $x$ and $a$ is a polynomial of $x$ defined as the product of the generator of $\operatorname{annIdeal}$ applied to $x$ and $a$ and $\operatorname{C}$ applied to $\operatorname{inv}$ applied to the leading coefficient of the generator of $\operatorname{annIdeal}$ applied to $x$ and $a$.

Mathlib.LinearAlgebra.Basis.Basic

Module.Basis.emptydefMathlib.LinearAlgebra.Basis.Basic, function or constant

Wording

no wording

English

Let $M$ be a set. Then $\operatorname{empty}$ applied to $M$ is a basis of $R$ and $M$ defined as $\operatorname{ofRepr}$ applied to $0$.

Module.Basis.mkdefMathlib.LinearAlgebra.Basis.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $v$. Assume that the top is less than or equal to the span of $R$ and the range of $v$. Then $\operatorname{mk}$ applied to $\mathrm{hli}$ and $\mathrm{hsp}$ is a basis of $R$ and $M$.

Module.Basis.singletondefMathlib.LinearAlgebra.Basis.Basic, function or constant

Wording

the singleton of x and R (from the name)

English

Let $x$ and $R$ be sets. Then the singleton of $x$ and $R$ is a basis of $R$ and $R$.

Module.Basis.spandefMathlib.LinearAlgebra.Basis.Basic, function or constant

Wording

the span of hli (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $v$. Then the span of $\mathrm{hli}$ is a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{range} (v))}{x_{4}})}$.

Mathlib.LinearAlgebra.Basis.Defs

Module.BasisstructureMathlib.LinearAlgebra.Basis.Defs, type

Wording

basis of R and M (from the name)

English

Let $x$, $R$ and $M$ be sets. Then the bases of $R$ and $M$ are a basic type.

Module.Basis.constrdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $M$. Let $S$ be a set. Then $\operatorname{constr}$ applied to $b$ and $S$ is a linear equivalence of the set of functions from elements of $x_{1}$ to elements of $\mathrm{M'}$ and the set of linear maps of $M$ and $\mathrm{M'}$.

Module.Basis.coorddefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the coordinate of b and i (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $i$ be an element of $x$. Then the coordinate of $b$ and $i$ is a linear map of $M$ and $R$ defined as the composition of $\operatorname{lapply}$ applied to $i$ and $\operatorname{toLinearMap}$ applied to the representation of $b$.

Module.Basis.equivdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the equivalence of e and #3 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $\mathrm{b'}$ be a basis of $R$ and $\mathrm{M'}$. Let $e$ be an equivalence from $x_{2}$ to $x$. Then the equivalence of $\mathrm{b'}$ and $e$ is a linear equivalence of $M$ and $\mathrm{M'}$ defined as the composition of the representation of $b$ and the inverse of the representation of the reindexing of $\mathrm{b'}$ and the inverse of $e$.

Module.Basis.equiv'defMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the equivalence of g and hf (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $\mathrm{b'}$ be a basis of $R$ and $\mathrm{M'}$. Let $f$ be a function from elements of $M$ to elements of $\mathrm{M'}$. Let $g$ be a function from elements of $\mathrm{M'}$ to elements of $M$. Assume that for all elements $i_{3}$ of $x_{1}$, $f$ applied to $b$ applied to $i_{3}$ is an element of the range of $\operatorname{coe}$ applied to $\mathrm{b'}$. Assume that for all elements $i_{2}$ of $x$, $g$ applied to $\mathrm{b'}$ applied to $i_{2}$ is an element of the range of $\operatorname{coe}$ applied to $b$. Assume that for all elements $i_{1}$ of $x_{1}$, $\EqtMACRoH {g (f (b (i_{1})))}{b (i_{1})}$. Assume that for all elements $i$ of $x$, $\EqtMACRoH {f (g (\mathrm{b'} (i)))}{\mathrm{b'} (i)}$. Then the equivalence of $f$ and $g$ is a linear equivalence of $M$ and $\mathrm{M'}$.

Module.Basis.equivFundefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the equivalence function of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the equivalence function of $b$ is a linear equivalence of $M$ and the set of functions from elements of $x$ to elements of $R$.

Module.Basis.mapdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the map of b and f (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $f$ be a linear equivalence of $M$ and $\mathrm{M'}$. Then the map of $b$ and $f$ is a basis of $R$ and $\mathrm{M'}$ defined as $\operatorname{ofRepr}$ applied to the composition of the inverse of $f$ and the representation of $b$.

Module.Basis.mapCoeffsdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $M$. Let $f$ be a ring isomorphism of $R$ and $\mathrm{R'}$ such that for all elements $c$ of $R$, for all elements $x_{6}$ of $M$, $\EqtMACRoH {\HSMulhSMulMACRoAL {f (c)}{x_{6}}}{\HSMulhSMulMACRoAL {c}{x_{6}}}$. Then $\operatorname{mapCoeffs}$ applied to $b$, $f$ and $h$ is a basis of $\mathrm{R'}$ and $M$ defined as $\operatorname{ofRepr}$ applied to the composition of $\operatorname{restrictScalars}$ applied to $\mathrm{R'}$ and the representation of $b$ and the linear equivalence of the inverse of the linear equivalence of the inverse of $f$.

Module.Basis.ofEquivFundefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the basis of e (from the name)

English

Let $e$ be a linear equivalence of $M$ and the set of functions from elements of $x$ to elements of $R$. Then the basis of $e$ is a basis of $R$ and $M$ defined as $\operatorname{ofRepr}$ applied to the composition of $e$ and the inverse of $\operatorname{linearEquivFunOnFinite}$ applied to $R$, $R$ and $x$.

Module.Basis.reindexdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the reindexing of b and e (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $e$ be an equivalence from $x$ to $x_{1}$. Then the reindexing of $b$ and $e$ is a basis of $R$ and $M$ defined as $\operatorname{ofRepr}$ applied to the composition of the representation of $b$ and the domain congruence of $e$.

Module.Basis.reindexFinsetRangedefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the reindexing finite set range of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the reindexing finite set range of $b$ is a basis of $R$ and $M$.

Module.Basis.reindexRangedefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the reindexing range of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the reindexing range of $b$ is a basis of $R$ and $M$ defined as $\mathrm{dite}$ applied to the proposition that $R$ is nontrivial, the function that maps $h$ to the reindexing of $b$ and the equivalence of $\operatorname{coe}$ applied to $b$ and $\operatorname{injective}$ applied to $b$ and the function that maps $h_{1}$ to $\operatorname{ofRepr}$ applied to the subsingleton equivalence of $M$ and the set of elements of the range of $\operatorname{coe}$ applied to $b$.

Module.Basis.reprdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the representation of self (from the name)

English

Let $\mathrm{self}$ be a basis of $R$ and $M$. Then the representation of $\mathrm{self}$ is a linear equivalence of $M$ and $\FinsuppMACRoQ {x}{R}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Module.Basis.sumCoordsdefMathlib.LinearAlgebra.Basis.Defs, function or constant

Wording

the sum of the coordinates of b (from the docstring)

English

Let $b$ be a basis of $R$ and $M$. Then the sum of the coordinates of $b$ is a linear map of $M$ and $R$ defined as the composition of $\operatorname{lsum}$ applied to $\Natural$ and the function that maps $x_{5}$ to the identity and $\operatorname{toLinearMap}$ applied to the representation of $b$.

Mathlib.LinearAlgebra.Basis.Exact

Module.Basis.ofSplitExactdefMathlib.LinearAlgebra.Basis.Exact, function or constant

Wording

the basis of v (from the name)

English

Assume that the composition of $s$ and $f$ is equal to the identity. 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$. Let $v$ be a basis of $R$ and $M$. Assume that $a$ is injective. Assume that for all elements $i$ of $x_{8}$, $\EqtMACRoH {s (v (a (i)))}{0}$. Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $s$ and $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $v$ and $b$. Assume that $\mathrm{Codisjoint}$ holds for the range of $a$ and the range of $b$. Then the basis of $v$ is a basis of $R$ and $P$.

Mathlib.LinearAlgebra.Basis.Fin

Module.Basis.finTwoProddefMathlib.LinearAlgebra.Basis.Fin, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{finTwoProd}$ applied to $R$ is a basis of $R$ and $\mathrm{Prod}$ applied to $R$ and $R$ defined as the basis of the inverse of $\operatorname{finTwoArrow}$ applied to $R$ and $R$.

Module.Basis.mkFinConsdefMathlib.LinearAlgebra.Basis.Fin, function or constant

Wording

no wording

English

Let $y$ be an element of $M$. Let $b$ be a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$. Assume that for all elements $c_{1}$ of $R$, for all elements $x_{3}$ of $M$, if $x_{3}$ is an element of $N$, then if $\EqtMACRoH {\HSMulhSMulMACRoAL {c_{1}}{y}+ x_{3}}{0}$, then $\EqtMACRoH {c_{1}}{0}$. Assume that for all elements $z$ of $M$, there exists an element $c$ of $R$, such that $z + \HSMulhSMulMACRoAL {c}{y}$ is an element of $N$. Then $\operatorname{mkFinCons}$ applied to $y$, $b$, $\mathrm{hli}$ and $\mathrm{hsp}$ is a basis of $R$ and $M$.

Module.Basis.mkFinConsOfLEdefMathlib.LinearAlgebra.Basis.Fin, function or constant

Wording

no wording

English

Let $y$ be an element of $M$ such that $y$ is an element of $O$. Let $b$ be a basis of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$. Assume that $N \leq O$. Assume that for all elements $c_{1}$ of $R$, for all elements $x_{4}$ of $M$, if $x_{4}$ is an element of $N$, then if $\HSMulhSMulMACRoAL {c_{1}}{y}+ x_{4}$ is equal to $0$, then $\EqtMACRoH {c_{1}}{0}$. Assume that for all elements $z$ of $M$, if $z$ is an element of $O$, then there exists an element $c$ of $R$, such that $z + \HSMulhSMulMACRoAL {c}{y}$ is an element of $N$. Then $\operatorname{mkFinConsOfLE}$ applied to $y$, $\mathrm{yO}$, $b$, $\mathrm{hNO}$, $\mathrm{hli}$ and $\mathrm{hsp}$ is a basis of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {O}{x_{3}})}$.

Module.Basis.mkFinSnocdefMathlib.LinearAlgebra.Basis.Fin, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$. Let $y$ be an element of $M$ such that for all elements $c_{1}$ of $R$, for all elements $x_{3}$ of $M$, if $x_{3}$ is an element of $N$, then if $\EqtMACRoH {\HSMulhSMulMACRoAL {c_{1}}{y}+ x_{3}}{0}$, then $\EqtMACRoH {c_{1}}{0}$ and for all elements $z$ of $M$, there exists an element $c$ of $R$ such that $z + \HSMulhSMulMACRoAL {c}{y}$ is an element of $N$. Then $\operatorname{mkFinSnoc}$ applied to $b$, $y$, $\mathrm{hli}$ and $\mathrm{hsp}$ is a basis of $R$ and $M$.

Module.Basis.mkFinSnocOfLEdefMathlib.LinearAlgebra.Basis.Fin, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$. Assume that $N \leq O$. Let $y$ be an element of $M$ such that $y$ is an element of $O$, for all elements $c_{1}$ of $R$, for all elements $x_{4}$ of $M$, if $x_{4}$ is an element of $N$, then if $\HSMulhSMulMACRoAL {c_{1}}{y}+ x_{4}$ is equal to $0$, then $\EqtMACRoH {c_{1}}{0}$ and for all elements $z$ of $M$, if $z$ is an element of $O$, then there exists an element $c$ of $R$ such that $z + \HSMulhSMulMACRoAL {c}{y}$ is an element of $N$. Then $\operatorname{mkFinSnocOfLE}$ applied to $b$, $\mathrm{hNO}$, $y$, $\mathrm{yO}$, $\mathrm{hli}$ and $\mathrm{hsp}$ is a basis of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {O}{x_{3}})}$.

Mathlib.LinearAlgebra.Basis.Flag

Module.Basis.flagdefMathlib.LinearAlgebra.Basis.Flag, function or constant

Wording

the flag of b and k (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $k$ be an element of $\mathrm{Fin}$ applied to $n + 1$. Then the flag of $b$ and $k$ is a submodule of $R$ and $M$ defined as the span of $R$ and the image of $\operatorname{coe}$ applied to $b$ and $\operatorname{ofPred}$ applied to the function that maps $i$ to $\mathrm{Lt} (\operatorname{castSucc} (i), k)$.

Module.Basis.toFlagdefMathlib.LinearAlgebra.Basis.Flag, function or constant

Wording

the flag of b (from the name)

English

Let $b$ be a basis of $K$ and $V$. Then the flag of $b$ is a flag of the set of submodules of $K$ and $V$.

Mathlib.LinearAlgebra.Basis.MulOpposite

Module.Basis.mulOppositedefMathlib.LinearAlgebra.Basis.MulOpposite, function or constant

Wording

the multiplicative opposite of b (from the docstring)

English

Let $b$ be a basis of $R$ and $H$. Then the multiplicative opposite of $b$ is a basis of $R$ and the set of multiplicative opposites of $H$ defined as the map of $b$ and the opposite linear equivalence of $R$.

Mathlib.LinearAlgebra.Basis.Prod

Module.Basis.proddefMathlib.LinearAlgebra.Basis.Prod, function or constant

Wording

the product of b and #2 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $\mathrm{b'}$ be a basis of $R$ and $\mathrm{M'}$. Then the product of $b$ and $\mathrm{b'}$ is a basis of $R$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ defined as $\operatorname{ofRepr}$ applied to the composition of the product congruence of the representation of $b$ and the representation of $\mathrm{b'}$ and the inverse of the sum finitely supported function equivalence product finitely supported function of $R$.

Mathlib.LinearAlgebra.Basis.SMul

Module.Basis.groupSMuldefMathlib.LinearAlgebra.Basis.SMul, function or constant

Wording

the group product of v and w (from the name)

English

Let $v$ be a basis of $R$ and $M$. Let $w$ be a function from elements of $x$ to elements of $G$. Then the group product of $v$ and $w$ is a basis of $R$ and $M$.

Module.Basis.isUnitSMuldefMathlib.LinearAlgebra.Basis.SMul, function or constant

Wording

no wording

English

Let $v$ be a basis of $R$ and $M$. Assume that for all elements $i$ of $x$, $w$ applied to $i$ is a unit. Then $\operatorname{isUnitSMul}$ applied to $v$ and $\mathrm{hw}$ is a basis of $R$ and $M$ defined as the unit product of $v$ and the function that maps $i$ to the unit of $\mathrm{hw}$ applied to $i$.

Module.Basis.unitsSMuldefMathlib.LinearAlgebra.Basis.SMul, function or constant

Wording

the unit product of v and w (from the name)

English

Let $v$ be a basis of $R$ and $M$. Let $w$ be a function from elements of $x$ to units of $R$. Then the unit product of $v$ and $w$ is a basis of $R$ and $M$.

Mathlib.LinearAlgebra.Basis.Submodule

Module.Basis.addSubgroupOfClosuredefMathlib.LinearAlgebra.Basis.Submodule, function or constant

Wording

the additive subgroup of A and b (from the name)

English

Let $A$ be an additive subgroup of $M$. Let $b$ be a basis of $R$ and $M$ such that $A$ is equal to the closure of the range of $\operatorname{coe}$ applied to $b$. Then the additive subgroup of $A$ and $b$ is a basis of $\Integer$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{toIntSubmodule} (A)}{x_{4}})}$.

Module.Basis.restrictScalarsdefMathlib.LinearAlgebra.Basis.Submodule, function or constant

Wording

no wording

English

Let $R$ be a set. Let $b$ be a basis of $S$ and $M$. Then $\operatorname{restrictScalars}$ applied to $R$ and $b$ is a basis of $R$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{range} (\operatorname{coe} (b)))}{x_{7}})}$.

Mathlib.LinearAlgebra.Basis.VectorSpace

LinearMap.leftInversedefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

the left inverse of f (from the docstring)

English

Let $f$ be a linear map of $V$ and $\mathrm{V'}$. Then the left inverse of $f$ is a linear map of $\mathrm{V'}$ and $V$ defined as $\mathrm{dite}$ applied to the proposition that the kernel of $f$ is equal to the bottom, the function that maps $\mathrm{h\_inj}$ to $\operatorname{choose}$ applied to $\mathrm{LinearMap\_\_exists\_leftInverse\_of\_injective}$ applied to $f$ and $\mathrm{h\_inj}$ and the function that maps $\mathrm{h\_inj1}$ to $0$.

Module.Basis.extenddefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

no wording

English

Assume that $\mathrm{LinearIndepOn}$ holds for $K$, $\mathrm{id}$ and $s$. Then $\operatorname{extend}$ applied to $\mathrm{hs}$ is a basis of $K$ and $V$.

Module.Basis.extendLedefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

no wording

English

Assume that $\mathrm{LinearIndepOn}$ holds for $K$, $\mathrm{id}$ and $s$. Assume that $s \leq t$. Assume that the top is less than or equal to the span of $K$ and $t$. Then $\operatorname{extendLe}$ applied to $\mathrm{hs}$, $\mathrm{hst}$ and $\mathrm{ht}$ is a basis of $K$ and $V$.

Module.Basis.ofSpandefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

the basis of hs (from the name)

English

Assume that the top is less than or equal to the span of $K$ and $s$. Then the basis of $\mathrm{hs}$ is a basis of $K$ and $V$.

Module.Basis.ofVectorSpacedefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

the basis of K and V (from the name)

English

Let $K$ and $V$ be sets. Then the basis of $K$ and $V$ is a basis of $K$ and $V$.

Module.Basis.ofVectorSpaceIndexdefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

the basis of K and V (from the name)

English

Let $K$ and $V$ be sets. Then the basis of $K$ and $V$ is an element of $\wp V$.

Module.Basis.sumExtenddefMathlib.LinearAlgebra.Basis.VectorSpace, function or constant

Wording

no wording

English

Assume that $\mathrm{LinearIndependent}$ holds for $K$ and $v$. Then $\operatorname{sumExtend}$ applied to $\mathrm{hs}$ is a basis of $K$ and $V$.

Mathlib.LinearAlgebra.BilinearForm.Basic

LinearMap.BilinForm.coeFnAddMonoidHomdefMathlib.LinearAlgebra.BilinearForm.Basic, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of bilinear forms of $R$ and $M$ and the set of functions from elements of $M$ and elements of $M$ to elements of $R$.

LinearMap.BilinForm.flipdefMathlib.LinearAlgebra.BilinearForm.Basic, function or constant

Wording

the flip of B (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then the flip of $B$ is a bilinear form of $R$ and $M$ defined as $\operatorname{flipHom}$ applied to $B$.

LinearMap.BilinForm.flipHomdefMathlib.LinearAlgebra.BilinearForm.Basic, function or constant

Wording

the flip (from the docstring)

English

The flip is a linear equivalence of the set of bilinear forms of $R$ and $M$ and the set of bilinear forms of $R$ and $M$ defined as $\operatorname{lflip}$.

LinearMap.BilinForm.restrictdefMathlib.LinearAlgebra.BilinearForm.Basic, function or constant

Wording

the restriction of B and W (from the docstring)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $W$ be a submodule of $R$ and $M$. Then the restriction of $B$ and $W$ is a bilinear form of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ defined as $\mathrm{LinearMap\_\_domRestrict\_u2081\_\_u2082\_}$ applied to $B$, $W$ and $W$.

Mathlib.LinearAlgebra.BilinearForm.DualLattice

LinearMap.BilinForm.dualSubmoduledefMathlib.LinearAlgebra.BilinearForm.DualLattice, function or constant

Wording

the dual submodule of B and N (from the docstring)

English

Let $B$ be a bilinear form of $S$ and $M$. Let $N$ be a submodule of $R$ and $M$. Then the dual submodule of $B$ and $N$ is a submodule of $R$ and $M$.

LinearMap.BilinForm.dualSubmodulePairingdefMathlib.LinearAlgebra.BilinearForm.DualLattice, function or constant

Wording

the dual submodule pairing of x6 and y (from the name)

English

Let $B$ be a bilinear form of $S$ and $M$. Let $x_{6}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{dualSubmodule} (B , N)}{x_{8}})}$. Let $y$ be an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {N}{x_{7}})}$. Then the dual submodule pairing of $x_{6}$ and $y$ is an element of $R$.

LinearMap.BilinForm.dualSubmoduleToDualdefMathlib.LinearAlgebra.BilinearForm.DualLattice, function or constant

Wording

the dual submodule to dual of B and N (from the name)

English

Let $B$ be a bilinear form of $S$ and $M$. Let $N$ be a submodule of $R$ and $M$. Then the dual submodule to dual of $B$ and $N$ is a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{dualSubmodule} (B , N)}{x_{6}})}$ and the set of duals of $R$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {N}{x_{7}})}$.

Mathlib.LinearAlgebra.BilinearForm.Hom

LinearEquiv.congrRight₂defMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the right congruence of e (from the name)

English

Let $e$ be a linear equivalence of $x_{3}$ and $x_{4}$. Then the right congruence of $e$ is a linear equivalence of the set of bilinear maps of $M$ and $x_{3}$ and the set of bilinear maps of $M$ and $x_{4}$ defined as the right congruence of the right congruence of $e$.

LinearMap.BilinForm.compdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the composition of l and r (from the name)

English

Let $B$ be a bilinear form of $R$ and $\mathrm{M'}$. Let $l$ and $r$ be linear maps of $M$ and $\mathrm{M'}$. Then the composition of $l$ and $r$ is a bilinear form of $R$ and $M$ defined as the complement of $l$ and $r$.

LinearMap.BilinForm.compLeftdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the left composition of B and f (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $f$ be a linear map of $M$ and $M$. Then the left composition of $B$ and $f$ is a bilinear form of $R$ and $M$ defined as the composition of $f$ and the identity.

LinearMap.BilinForm.compRightdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the right composition of B and f (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $f$ be a linear map of $M$ and $M$. Then the right composition of $B$ and $f$ is a bilinear form of $R$ and $M$ defined as the composition of the identity and $f$.

LinearMap.BilinForm.congrdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the congruence of e (from the name)

English

Let $e$ be a linear equivalence of $M$ and $\mathrm{M'}$. Then the congruence of $e$ is a linear equivalence of the set of bilinear forms of $R$ and $M$ and the set of bilinear forms of $R$ and $\mathrm{M'}$ defined as the composition of the right congruence of the left congruence of $e$ and the left congruence of $e$.

LinearMap.BilinForm.linMulLindefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

no wording

English

Let $f$ and $g$ be linear maps of $M$ and $R$. Then $\operatorname{linMulLin}$ applied to $f$ and $g$ is a bilinear form of $R$ and $M$ defined as the complement of $f$ and $g$.

LinearMap.BilinForm.toLinHomFlipdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the linear homomorphism flip (from the name)

English

The linear homomorphism flip is a linear map of the set of bilinear forms of $R$ and $M$ and the set of linear maps of $M$ and the set of linear maps of $M$ and $R$ defined as $\operatorname{toLinearMap}$ applied to the flip.

LinearMap.compBilinFormdefMathlib.LinearAlgebra.BilinearForm.Hom, function or constant

Wording

the composition bilinear form of f and B (from the name)

English

Let $f$ be a linear map of $R$ and $\mathrm{R'}$. Let $B$ be a bilinear form of $R$ and $M$. Then the composition bilinear form of $f$ and $B$ is a bilinear form of $\mathrm{R'}$ and $M$ defined as $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to $\mathrm{LinearMap\_\_restrictScalars\_u2081\_\_u2082\_}$ applied to $\mathrm{R'}$, $\mathrm{R'}$ and $B$ and $f$.

Mathlib.LinearAlgebra.BilinearForm.Isometry

LinearMap.BilinForm.IsometrystructureMathlib.LinearAlgebra.BilinearForm.Isometry, type

Wording

isometry of x7 and x8 (from the name)

English

Let $x_{7}$ be a bilinear form of $R$ and $x$. Let $x_{8}$ be a bilinear form of $R$ and $x_{1}$. Then the isometries of $x_{7}$ and $x_{8}$ are a basic type.

LinearMap.BilinForm.Isometry.compdefMathlib.LinearAlgebra.BilinearForm.Isometry, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be an isometry of $x_{11}$ and $x_{12}$. Let $f$ be an isometry of $x_{10}$ and $x_{11}$. Then the composition of $g$ and $f$ is an isometry of $x_{10}$ and $x_{12}$.

LinearMap.BilinForm.Isometry.iddefMathlib.LinearAlgebra.BilinearForm.Isometry, function or constant

Wording

the identity isometry of B (from the docstring)

English

Let $B$ be a bilinear form of $R$ and $M$. Then the identity isometry of $B$ is an isometry of $B$ and $B$.

LinearMap.BilinForm.Isometry.ofEqdefMathlib.LinearAlgebra.BilinearForm.Isometry, function or constant

Wording

the isometry of h (from the name)

English

Assume that $\EqtMACRoH {x_{4}}{x_{5}}$. Then the isometry of $h$ is an isometry of $x_{4}$ and $x_{5}$.

Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv

LinearMap.BilinForm.EquivalentdefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, predicate

Wording

x7 is equivalent to x8 (from the name)

English

Let $x_{7}$ be a bilinear form of $R$ and $x$. Let $x_{8}$ be a bilinear form of $R$ and $x_{1}$. Then $x_{7}$ is equivalent to $x_{8}$, if $\mathrm{Nonempty}$ holds for the set of isometry equivalences of $x_{7}$ and $x_{8}$.

LinearMap.BilinForm.IsometryEquivstructureMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, type

Wording

isometry equivalence of x7 and x8 (from the name)

English

Let $x_{7}$ be a bilinear form of $R$ and $x$. Let $x_{8}$ be a bilinear form of $R$ and $x_{1}$. Then the isometry equivalences of $x_{7}$ and $x_{8}$ are a basic type.

LinearMap.BilinForm.IsometryEquiv.refldefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, function or constant

Wording

the identity of B (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then the identity of $B$ is an isometry equivalence of $B$ and $B$.

LinearMap.BilinForm.IsometryEquiv.symmdefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, function or constant

Wording

the inverse isometric equivalence of f (from the docstring)

English

Let $f$ be an isometry equivalence of $x_{7}$ and $x_{8}$. Then the inverse isometric equivalence of $f$ is an isometry equivalence of $x_{8}$ and $x_{7}$.

LinearMap.BilinForm.IsometryEquiv.toIsometrydefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, function or constant

Wording

the isometry of g (from the name)

English

Let $g$ be an isometry equivalence of $x_{7}$ and $x_{8}$. Then the isometry of $g$ is an isometry of $x_{7}$ and $x_{8}$.

LinearMap.BilinForm.IsometryEquiv.transdefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be an isometry equivalence of $x_{10}$ and $x_{11}$. Let $g$ be an isometry equivalence of $x_{11}$ and $x_{12}$. Then the composition of $f$ and $g$ is an isometry equivalence of $x_{10}$ and $x_{12}$.

LinearMap.BilinForm.isometryEquivOfCompLinearEquivdefMathlib.LinearAlgebra.BilinearForm.IsometryEquiv, function or constant

Wording

the isometry equivalence of B and f (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $f$ be a linear equivalence of $x$ and $M$. Then the isometry equivalence of $B$ and $f$ is an isometry equivalence of $B$ and the composition of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{toLinearMap}$ applied to $f$.

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

LinearMap.BilinForm.iIsOrthodefMathlib.LinearAlgebra.BilinearForm.Orthogonal, predicate

Wording

no wording

English

Let $B$ be a bilinear form of $R$ and $M$. Let $v$ be a function from elements of $n$ to elements of $M$. Then $\operatorname{iIsOrtho}$ holds for $B$ and $v$, if $\mathrm{LinearMap\_\_IsOrtho\_u1d62\_}$ holds for $B$ and $v$.

LinearMap.BilinForm.orthogonaldefMathlib.LinearAlgebra.BilinearForm.Orthogonal, function or constant

Wording

the orthogonal complement of B and N (from the docstring)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $N$ be a submodule of $R$ and $M$. Then the orthogonal complement of $B$ and $N$ is a submodule of $R$ and $M$ defined as the orthogonal complement of $B$ and $N$.

Mathlib.LinearAlgebra.BilinearForm.Properties

LinearMap.BilinForm.IsAltdefMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

no wording

English

Let $B$ be a bilinear form of $R$ and $M$. Then $\operatorname{IsAlt}$ holds for $B$, if $\operatorname{IsAlt}$ holds for $B$.

LinearMap.BilinForm.IsNonnegstructureMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

B is nonnegative (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then we can say that $B$ is nonnegative.

LinearMap.BilinForm.IsPosSemidefstructureMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

no wording

English

Let $B$ be a bilinear form of $R$ and $M$. Then we can say that $\operatorname{IsPosSemidef}$ holds for $B$.

LinearMap.BilinForm.IsRefldefMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

B is a identity (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then $B$ is an identity, if $B$ is an identity.

LinearMap.BilinForm.IsSymmstructureMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

B is inverse (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then we can say that $B$ is inverse.

LinearMap.BilinForm.NondegeneratedefMathlib.LinearAlgebra.BilinearForm.Properties, predicate

Wording

B is a nondegenerate (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then $B$ is a nondegenerate, if $B$ is non-degenerate.

LinearMap.BilinForm.dualBasisdefMathlib.LinearAlgebra.BilinearForm.Properties, function or constant

Wording

the dual basis of B and b (from the name)

English

Let $B$ be a bilinear form of $K$ and $V$ such that $B$ is a nondegenerate. Let $b$ be a basis of $K$ and $V$. Then the dual basis of $B$ and $b$ is a basis of $K$ and $V$ defined as the map of the dual basis of $b$ and the inverse of the dual of $B$ and $\mathrm{hB}$.

LinearMap.BilinForm.leftAdjointOfNondegeneratedefMathlib.LinearAlgebra.BilinearForm.Properties, function or constant

Wording

the left adjoint of B and x3 (from the name)

English

Let $B$ be a bilinear form of $K$ and $V$ such that $B$ is a nondegenerate. Let $x_{3}$ be a linear map of $V$ and $V$. Then the left adjoint of $B$ and $x_{3}$ is a linear map of $V$ and $V$ defined as the inverse composition of the right composition of $B$ and $x_{3}$ and $B$.

LinearMap.BilinForm.symmCompOfNondegeneratedefMathlib.LinearAlgebra.BilinearForm.Properties, function or constant

Wording

the inverse composition of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be bilinear forms of $K$ and $V$ such that $x_{4}$ is a nondegenerate. Then the inverse composition of $x_{3}$ and $x_{4}$ is a linear map of $V$ and $V$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the dual of $x_{4}$ and $h_{1}$ and $x_{3}$.

LinearMap.BilinForm.toDualdefMathlib.LinearAlgebra.BilinearForm.Properties, function or constant

Wording

the dual of B and b (from the name)

English

Let $B$ be a bilinear form of $K$ and $V$ such that $B$ is a nondegenerate. Then the dual of $B$ and $b$ is a linear equivalence of $V$ and the set of duals of $K$ and $V$.

Mathlib.LinearAlgebra.BilinearForm.TensorProduct

LinearMap.BilinForm.baseChangedefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

the base change of A and B (from the docstring)

English

Let $A$ be a set. Let $B$ be a bilinear form of $R$ and $x$. Then the base change of $A$ and $B$ is a bilinear form of $A$ and the set of tensor products of $A$ and $x$ defined as $\operatorname{tmul}$ applied to the product of $A$ and $A$ and $B$.

LinearMap.BilinForm.tensorDistribdefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

no wording

English

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 bilinear forms of $A$ and $x$ and the set of bilinear forms of $R$ and $x_{1}$ and the set of bilinear forms of $A$ and the set of tensor products of $x$ and $x_{1}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the right congruence of $\operatorname{rid}$ applied to $R$, $A$ and $A$ and $\operatorname{tensorDistrib}$ applied to $R$ and $A$.

LinearMap.BilinForm.tensorDistribEquivdefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

the tensor distributive equivalence of R (from the name)

English

Let $R$ be a set. Then the tensor distributive equivalence of $R$ is a linear equivalence of the set of tensor products of the set of bilinear forms of $R$ and $x$ and the set of bilinear forms of $R$ and $x_{1}$ and the set of bilinear forms of $R$ and the set of tensor products of $x$ and $x_{1}$ defined as the composition of the composition of the composition of the congruence of the equivalence of the identity ring homomorphism of $R$ and the equivalence of the identity ring homomorphism of $R$ and the dual distributive equivalence of the set of tensor products of $x$ and $x$ and the set of tensor products of $x_{1}$ and $x_{1}$ and the dual map of $\operatorname{tensorTensorTensorComm}$ applied to $R$, $x$, $x_{1}$, $x$ and $x_{1}$ and the inverse of the equivalence of the identity ring homomorphism of $R$.

LinearMap.BilinForm.tmuldefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

no wording

English

Let $x_{10}$ be a bilinear form of $A$ and $x$. Let $x_{11}$ be a bilinear map of $x_{1}$ and $R$. Then $\operatorname{tmul}$ applied to $x_{10}$ and $x_{11}$ is a bilinear map of the set of tensor products of $x$ and $x_{1}$ and $A$ defined as $\operatorname{tensorDistrib}$ applied to $R$, $A$ and $\operatorname{tmul}$ applied to $R$, $x_{10}$ and $x_{11}$.

LinearMap.BilinMap.baseChangedefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

the base change of A and B (from the docstring)

English

Let $A$ be a set. Let $B$ be a bilinear map of $x$ and $x_{1}$. Then the base change of $A$ and $B$ is a bilinear map of the set of tensor products of $A$ and $x$ and the set of tensor products of $A$ and $x_{1}$ defined as $\operatorname{tmul}$ applied to the product of $A$ and $A$ and $B$.

LinearMap.BilinMap.tensorDistribdefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

no wording

English

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 bilinear maps of $x$ and $x_{2}$ and the set of bilinear maps of $x_{1}$ and $x_{3}$ and the set of bilinear 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 $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of the identity ring homomorphism of $A$ and the composition of $\operatorname{flip}$ applied to $\operatorname{llcomp}$ applied to $A$, the set of tensor products of the set of tensor products of $x$ and $x_{1}$ and the set of tensor products of $x$ and $x_{1}$, the set of tensor products of the set of tensor products of $x$ and $x$ and the set of tensor products of $x_{1}$ and $x_{1}$ and the set of tensor products of $x_{2}$ and $x_{3}$ and $\operatorname{toLinearMap}$ applied to $\operatorname{tensorTensorTensorComm}$ applied to $R$, $R$, $A$, $A$, $x$, $x_{1}$, $x$ and $x_{1}$ and the composition of the homomorphism tensor homomorphism map of $x_{2}$ and $x_{3}$ and $\operatorname{toLinearMap}$ applied to the congruence of the equivalence of the identity ring homomorphism of $A$ and the equivalence of the identity ring homomorphism of $R$.

LinearMap.BilinMap.tmuldefMathlib.LinearAlgebra.BilinearForm.TensorProduct, function or constant

Wording

no wording

English

Let $x_{17}$ be a bilinear map of $x$ and $x_{2}$. Let $x_{18}$ be a bilinear map of $x_{1}$ and $x_{3}$. Then $\operatorname{tmul}$ applied to $x_{17}$ and $x_{18}$ is a bilinear 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_{17}$ and $x_{18}$.

Mathlib.LinearAlgebra.BilinearMap

IsBilinearMapstructureMathlib.LinearAlgebra.BilinearMap, predicate

Wording

f is a bilinear map (from the name)

English

Let $R$ be a set. Let $f$ be a function from elements of $E$ and elements of $F$ to elements of $G$. Then we can say that $f$ is a bilinear map.

IsBilinearMap.toLinearMapdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

the linear map of hf (from the name)

English

Assume that $f$ is a bilinear map. Then the linear map of $\mathrm{hf}$ is a linear map of $E$ and the set of linear maps of $F$ and $G$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $R$, $f$, $\mathrm{IsBilinearMap\_\_add\_left}$ applied to $\mathrm{hf}$, $\mathrm{IsBilinearMap\_\_smul\_left}$ applied to $\mathrm{hf}$, $\mathrm{IsBilinearMap\_\_add\_right}$ applied to $\mathrm{hf}$ and $\mathrm{IsBilinearMap\_\_smul\_right}$ applied to $\mathrm{hf}$.

LinearMap.BilinFormdefMathlib.LinearAlgebra.BilinearMap, type

Wording

bilinear form of R and M (from the name)

English

Let $R$ and $M$ be sets. Then a bilinear form of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of bilinear maps of $M$ and $R$.

LinearMap.BilinMapdefMathlib.LinearAlgebra.BilinearMap, type

Wording

bilinear map of M and x1 (from the name)

English

Let $R$, $M$ and $x_{1}$ be sets. Then a bilinear map of $M$ and $x_{1}$ is an element of the function that maps $R$, $M$ and $x_{1}$ to the set of linear maps of $M$ and the set of linear maps of $M$ and $x_{1}$.

LinearMap.compl₁₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

the complement of g and #3 (from the name)

English

Let $f$ be a linear map of $x_{4}$ and the set of linear maps of $N$ and $x_{5}$. Let $g$ be a linear map of $x_{6}$ and $x_{4}$. Let $\mathrm{g'}$ be a linear map of $x_{7}$ and $N$. Then the complement of $g$ and $\mathrm{g'}$ is a linear map of $x_{6}$ and the set of linear maps of $x_{7}$ and $x_{5}$ defined as the complement of the composition of $f$ and $g$ and $\mathrm{g'}$.

LinearMap.compl₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

the complement of h2 and g (from the name)

English

Let $h_{2}$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Let $g$ be a linear map of $Q$ and $N$. Then the complement of $h_{2}$ and $g$ is a linear map of $M$ and the set of linear maps of $Q$ and $P$.

LinearMap.compr₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and the set of linear maps of $x_{2}$ and $x_{3}$. Let $g$ be a linear map of $x_{3}$ and $x_{4}$. Then $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to $f$ and $g$ is a linear map of $M$ and the set of linear maps of $x_{2}$ and $x_{4}$.

LinearMap.compr₂ₛₗdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Let $g$ be a linear map of $P$ and $Q$. Then $\mathrm{LinearMap\_\_compr\_u2082\_\_u209b\_\_u2097\_}$ applied to $f$ and $g$ is a linear map of $M$ and the set of linear maps of $N$ and $Q$ defined as the composition of $\operatorname{llcomp}$ applied to $x_{3}$, $N$, $P$, $Q$ and $g$ and $f$.

LinearMap.domRestrict₁₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $S$ and $N$. Then $\mathrm{LinearMap\_\_domRestrict\_u2081\_\_u2082\_}$ applied to $f$, $p$ and $q$ is a linear map of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {p}{x_{15}})}$ and the set of linear maps of $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {q}{x_{16}})}$ and $P$ defined as $\mathrm{LinearMap\_\_domRestrict\_u2082\_}$ applied to the restriction of $f$ and $p$ and $q$.

LinearMap.domRestrict₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Let $q$ be a submodule of $S$ and $N$. Then $\mathrm{LinearMap\_\_domRestrict\_u2082\_}$ applied to $f$ and $q$ is a linear map of $M$ and the set of linear maps of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {q}{x_{15}})}$ and $P$.

LinearMap.flipdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

the flip of f (from the name)

English

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

LinearMap.lcompdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $S$ and $N$ be sets. Let $f$ be a linear map of $M$ and $x_{2}$. Then $\operatorname{lcomp}$ applied to $S$, $N$ and $f$ is a linear map of the set of linear maps of $x_{2}$ and $N$ and the set of linear maps of $M$ and $N$ defined as $\mathrm{LinearMap\_\_lcomp\_u209b\_\_u2097\_}$ applied to $S$, $N$, the identity ring homomorphism of $R$ and $f$.

LinearMap.lcompₛₗdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $x_{2}$ and $P$ be sets. Let $x_{8}$ be a ring homomorphism of $x$ and $x_{1}$. Let $f$ be a linear map of $M$ and $N$. Then $\mathrm{LinearMap\_\_lcomp\_u209b\_\_u2097\_}$ applied to $x_{2}$, $P$, $x_{8}$ and $f$ is a linear map of the set of linear maps of $N$ and $P$ and the set of linear maps of $M$ and $P$ defined as the flip of the composition of the flip of the identity and $f$.

LinearMap.lflipdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

$\operatorname{lflip}$ 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 $N$ and the set of linear maps of $M$ and $P$.

LinearMap.llcompdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $x_{2}$, $M$, $N$ and $P$ be sets. Then $\operatorname{llcomp}$ applied to $x_{2}$, $M$, $N$ and $P$ is a linear map of the set of linear maps of $N$ and $P$ and the set of linear maps of the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $P$.

LinearMap.lsmuldefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\operatorname{lsmul}$ applied to $R$ and $M$ is a linear map of $R$ and the set of linear maps of $M$ and $M$.

LinearMap.mk₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a function from elements of $M$ and elements of $x_{1}$ to elements of $x_{2}$ such that for all elements $x_{11}$ of $M$, for all elements $x_{12}$ of $M$, for all elements $n_{2}$ of $x_{1}$, $\EqtMACRoH {f (x_{11} + x_{12} , n_{2})}{f (x_{11} , n_{2})+ f (x_{12} , n_{2})}$, for all elements $c_{1}$ of $R$, for all elements $m_{2}$ of $M$, for all elements $n_{1}$ of $x_{1}$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {c_{1}}{m_{2}}, n_{1})}{\HSMulhSMulMACRoAL {c_{1}}{f (m_{2} , n_{1})}}$, for all elements $m_{1}$ of $M$, for all elements $x_{9}$ of $x_{1}$, for all elements $x_{10}$ of $x_{1}$, $\EqtMACRoH {f (m_{1} , x_{9} + x_{10})}{f (m_{1} , x_{9})+ f (m_{1} , x_{10})}$ and for all elements $c$ of $R$, for all elements $m$ of $M$, for all elements $n$ of $x_{1}$, $\EqtMACRoH {f (m , \HSMulhSMulMACRoAL {c}{n})}{\HSMulhSMulMACRoAL {c}{f (m , n)}}$. Then $\mathrm{LinearMap\_\_mk\_u2082\_}$ applied to $R$, $f$, $H_{1}$, $H_{2}$, $H_{3}$ and $H_{4}$ is a linear map of $M$ and the set of linear maps of $x_{1}$ and $x_{2}$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_'}$ applied to $R$, $R$, $f$, $H_{1}$, $H_{2}$, $H_{3}$ and $H_{4}$.

LinearMap.mk₂'defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $R$ and $S$ be sets. Let $f$ be a function from elements of $M$ and elements of $N$ to elements of $x_{2}$ such that for all elements $x_{12}$ of $M$, for all elements $x_{13}$ of $M$, for all elements $n_{2}$ of $N$, $\EqtMACRoH {f (x_{12} + x_{13} , n_{2})}{f (x_{12} , n_{2})+ f (x_{13} , n_{2})}$, for all elements $c_{1}$ of $R$, for all elements $m_{2}$ of $M$, for all elements $n_{1}$ of $N$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {c_{1}}{m_{2}}, n_{1})}{\HSMulhSMulMACRoAL {c_{1}}{f (m_{2} , n_{1})}}$, for all elements $m_{1}$ of $M$, for all elements $x_{10}$ of $N$, for all elements $x_{11}$ of $N$, $\EqtMACRoH {f (m_{1} , x_{10} + x_{11})}{f (m_{1} , x_{10})+ f (m_{1} , x_{11})}$ and for all elements $c$ of $S$, for all elements $m$ of $M$, for all elements $n$ of $N$, $\EqtMACRoH {f (m , \HSMulhSMulMACRoAL {c}{n})}{\HSMulhSMulMACRoAL {c}{f (m , n)}}$. Then $\mathrm{LinearMap\_\_mk\_u2082\_'}$ applied to $R$, $S$, $f$, $H_{1}$, $H_{2}$, $H_{3}$ and $H_{4}$ is a linear map of $M$ and the set of linear maps of $N$ and $x_{2}$ defined as $\mathrm{LinearMap\_\_mk\_u2082\_'\_u209b\_\_u2097\_}$ applied to the identity ring homomorphism of $R$, the identity ring homomorphism of $S$, $f$, $H_{1}$, $H_{2}$, $H_{3}$ and $H_{4}$.

LinearMap.mk₂'ₛₗdefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $x_{13}$ be a ring homomorphism of $R$ and $x$. Let $x_{14}$ be a ring homomorphism of $S$ and $x_{1}$. Let $f$ be a function from elements of $M$ and elements of $N$ to elements of $P$ such that for all elements $x_{17}$ of $M$, for all elements $x_{18}$ of $M$, for all elements $n_{2}$ of $N$, $\EqtMACRoH {f (x_{17} + x_{18} , n_{2})}{f (x_{17} , n_{2})+ f (x_{18} , n_{2})}$, for all elements $c_{1}$ of $R$, for all elements $m_{2}$ of $M$, for all elements $n_{1}$ of $N$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {c_{1}}{m_{2}}, n_{1})}{\HSMulhSMulMACRoAL {x_{13} (c_{1})}{f (m_{2} , n_{1})}}$, for all elements $m_{1}$ of $M$, for all elements $x_{15}$ of $N$, for all elements $x_{16}$ of $N$, $\EqtMACRoH {f (m_{1} , x_{15} + x_{16})}{f (m_{1} , x_{15})+ f (m_{1} , x_{16})}$ and for all elements $c$ of $S$, for all elements $m$ of $M$, for all elements $n$ of $N$, $\EqtMACRoH {f (m , \HSMulhSMulMACRoAL {c}{n})}{\HSMulhSMulMACRoAL {x_{14} (c)}{f (m , n)}}$. Then $\mathrm{LinearMap\_\_mk\_u2082\_'\_u209b\_\_u2097\_}$ applied to $x_{13}$, $x_{14}$, $f$, $H_{1}$, $H_{2}$, $H_{3}$ and $H_{4}$ is a linear map of $M$ and the set of linear maps of $N$ and $P$.

LinearMap.restrictScalarsRangedefMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $i$ be a linear map of $\mathrm{M'}$ and $M$. Let $k$ be a linear map of $\mathrm{P'}$ and $P$ such that $\operatorname{coe}$ applied to $k$ is injective. Let $f$ be a linear map of $M$ and $P$ such that for all elements $m$ of $\mathrm{M'}$, $f$ applied to $i$ applied to $m$ is an element of the range of $k$. Then $\operatorname{restrictScalarsRange}$ applied to $i$, $k$, $\mathrm{hk}$, $f$ and $\mathrm{hf}$ is a linear map of $\mathrm{M'}$ and $\mathrm{P'}$ defined as the codomain lift of the composition of $\operatorname{restrictScalars}$ applied to $S$ and $f$ and $i$ and $k$.

LinearMap.restrictScalarsRange₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $i$ be a linear map of $\mathrm{M'}$ and $M$. Let $j$ be a linear map of $\mathrm{N'}$ and $N$. Let $k$ be a linear map of $\mathrm{P'}$ and $P$ such that $\operatorname{coe}$ applied to $k$ is injective. Let $B$ be a linear map of $M$ and the set of linear maps of $N$ and $P$ such that for all elements $m$ of $\mathrm{M'}$, for all elements $n$ of $\mathrm{N'}$, $\operatorname{coe}$ applied to $B$, $i$ applied to $m$ and $j$ applied to $n$ is an element of the range of $k$. Then $\mathrm{LinearMap\_\_restrictScalarsRange\_u2082\_}$ applied to $i$, $j$, $k$, $\mathrm{hk}$, $B$ and $\mathrm{hB}$ is a linear map of $\mathrm{M'}$ and the set of linear maps of $\mathrm{N'}$ and $\mathrm{P'}$ defined as $\mathrm{LinearMap\_\_codRestrict\_u2082\_}$ applied to the complement of $i$ and $j$, $k$, $\mathrm{hk}$ and $\mathrm{hB}$.

LinearMap.restrictScalars₁₂defMathlib.LinearAlgebra.BilinearMap, function or constant

Wording

no wording

English

Let $\mathrm{R'}$ and $\mathrm{S'}$ be sets. Let $B$ be a linear map of $M$ and the set of linear maps of $N$ and $x_{2}$. Then $\mathrm{LinearMap\_\_restrictScalars\_u2081\_\_u2082\_}$ applied to $\mathrm{R'}$, $\mathrm{S'}$ and $B$ is a linear map of $M$ and the set of linear maps of $N$ and $x_{2}$.

Mathlib.LinearAlgebra.Charpoly.Basic

LinearMap.charpolydefMathlib.LinearAlgebra.Charpoly.Basic, function or constant

Wording

the characteristic polynomial of f (from the docstring)

English

Let $f$ be a linear map of $M$ and $M$. Then the characteristic polynomial of $f$ is a polynomial of $R$ defined as the characteristic polynomial of $\operatorname{toMatrix}$ applied to $\operatorname{chooseBasis}$ applied to $R$ and $M$, $\operatorname{chooseBasis}$ applied to $R$ and $M$ and $f$.

Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

CliffordAlgebra.equivBaseChangedefMathlib.LinearAlgebra.CliffordAlgebra.BaseChange, function or constant

Wording

the equivalence base change of A and Q (from the name)

English

Let $A$ be a set. Let $Q$ be a quadratic form of $R$ and $V$. Then the equivalence base change of $A$ and $Q$ is an algebra isomorphism of the set of Clifford algebras of the base change of $A$ and $Q$ and the set of tensor products of $A$ and the set of Clifford algebras of $Q$ defined as the algebra isomorphism of the base change of $A$ and $Q$ and the Clifford algebra of $A$ and $Q$.

CliffordAlgebra.ofBaseChangedefMathlib.LinearAlgebra.CliffordAlgebra.BaseChange, function or constant

Wording

the Clifford algebra of A and Q (from the name)

English

Let $A$ be a set. Let $Q$ be a quadratic form of $R$ and $V$. Then the Clifford algebra of $A$ and $Q$ is an algebra homomorphism of the set of tensor products of $A$ and the set of Clifford algebras of $Q$ and the set of Clifford algebras of the base change of $A$ and $Q$.

CliffordAlgebra.toBaseChangedefMathlib.LinearAlgebra.CliffordAlgebra.BaseChange, function or constant

Wording

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

English

Let $A$ be a set. Let $Q$ be a quadratic form of $R$ and $V$. Then the base change of $A$ and $Q$ is an algebra homomorphism of the set of Clifford algebras of the base change of $A$ and $Q$ and the set of tensor products of $A$ and the set of Clifford algebras of $Q$ defined as $\operatorname{lift}$ applied to the base change of $A$ and $Q$ and the map of the identity and the inclusion of $Q$.

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

CliffordAlgebradefMathlib.LinearAlgebra.CliffordAlgebra.Basic, type

Wording

Clifford algebra of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then a Clifford algebra of $Q$ is an element of the function that maps $Q$ to the set of quotients of the ring congruence relation of $Q$.

CliffordAlgebra.RelinductiveMathlib.LinearAlgebra.CliffordAlgebra.Basic, predicate

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $x_{3}$ and $x_{4}$ be tensor algebras of $R$ and $M$. Then we can say that $\operatorname{Rel}$ holds for $Q$, $x_{3}$ and $x_{4}$.

CliffordAlgebra.equivOfIsometrydefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be an isometry equivalence of $x_{7}$ and $x_{8}$. Then the equivalence of $e$ is an algebra isomorphism of the set of Clifford algebras of $x_{7}$ and the set of Clifford algebras of $x_{8}$.

CliffordAlgebra.liftdefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

the lift of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the lift of $Q$ is an equivalence from $\SubtypeSet {f}{\mathrm{forall} (M , \lambda m . \EqtMACRoH {(f (m)\times f (m))}{\operatorname{algebraMap} (R , A , Q (m))})}$ to the set of algebra homomorphisms of the set of Clifford algebras of $Q$ and $A$.

CliffordAlgebra.mapdefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

the map of f (from the name)

English

Let $f$ be an isometry of $x_{7}$ and $x_{8}$. Then the map of $f$ is an algebra homomorphism of the set of Clifford algebras of $x_{7}$ and the set of Clifford algebras of $x_{8}$ defined as $\operatorname{lift}$ applied to $x_{7}$ and the composition of the inclusion of $x_{8}$ and $\operatorname{toLinearMap}$ applied to $f$.

CliffordAlgebra.ringCondefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

the ring congruence relation of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the ring congruence relation of $Q$ is a ring congruence relation of the set of tensor algebras of $R$ and $M$ defined as the ring congruence relation generator of $\operatorname{Rel}$ applied to $Q$.

CliffordAlgebra.ιdefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

the inclusion of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the inclusion of $Q$ is a linear map of $M$ and the set of Clifford algebras of $Q$ defined as the composition of the linear map of $\mathrm{RingCon\_\_mk\_u2090\_}$ applied to $R$ and the ring congruence relation of $Q$ and the inclusion of $R$.

TensorAlgebra.toClifforddefMathlib.LinearAlgebra.CliffordAlgebra.Basic, function or constant

Wording

no wording

English

$\operatorname{toClifford}$ is an algebra homomorphism of the set of tensor algebras of $R$ and $M$ and the set of Clifford algebras of $Q$ defined as $\operatorname{lift}$ applied to $R$ and the inclusion of $Q$.

Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory

QuadraticModuleCat.cliffordAlgebradefMathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory, function or constant

Wording

the Clifford algebra (from the name)

English

The Clifford algebra is a functor of the set of quadratic module categories of $R$ and the set of algebra categories of $R$.

Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation

CliffordAlgebra.involutedefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

no wording

English

$\operatorname{involute}$ is an algebra homomorphism of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $Q$ defined as $\operatorname{lift}$ applied to $Q$ and $\operatorname{neg}$ applied to the inclusion of $Q$.

CliffordAlgebra.involuteEquivdefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

the involute equivalence (from the name)

English

The involute equivalence is an algebra isomorphism of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $Q$.

CliffordAlgebra.reversedefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

the reverse (from the name)

English

The reverse is a linear map of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $Q$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the opposite linear equivalence of $R$ and the linear map of the reverse opposite.

CliffordAlgebra.reverseEquivdefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

the reverse equivalence (from the name)

English

The reverse equivalence is a linear equivalence of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $Q$ defined as the linear equivalence of the reverse and $\mathrm{CliffordAlgebra\_\_reverse\_involutive}$.

CliffordAlgebra.reverseOpdefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

the reverse opposite (from the name)

English

The reverse opposite is an algebra homomorphism of the set of Clifford algebras of $Q$ and the set of multiplicative opposites of the set of Clifford algebras of $Q$ defined as $\operatorname{lift}$ applied to $Q$ and the composition of $\operatorname{toLinearMap}$ applied to the opposite linear equivalence of $R$ and the inclusion of $Q$.

CliffordAlgebra.reverseOpEquivdefMathlib.LinearAlgebra.CliffordAlgebra.Conjugation, function or constant

Wording

the reverse opposite equivalence (from the name)

English

The reverse opposite equivalence is an algebra isomorphism of the set of Clifford algebras of $Q$ and the set of multiplicative opposites of the set of Clifford algebras of $Q$.

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

CliffordAlgebra.changeFormdefMathlib.LinearAlgebra.CliffordAlgebra.Contraction, function or constant

Wording

the change form of h (from the name)

English

Assume that the quadratic map of $B$ is equal to $\mathrm{Q'} - Q$. Then the change form of $h$ is a linear map of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $\mathrm{Q'}$.

CliffordAlgebra.changeFormEquivdefMathlib.LinearAlgebra.CliffordAlgebra.Contraction, function or constant

Wording

the change form equivalence of h (from the name)

English

Assume that the quadratic map of $B$ is equal to $\mathrm{Q'} - Q$. Then the change form equivalence of $h$ is a linear equivalence of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $\mathrm{Q'}$.

CliffordAlgebra.contractLeftdefMathlib.LinearAlgebra.CliffordAlgebra.Contraction, function or constant

Wording

no wording

English

$\operatorname{contractLeft}$ is a linear map of the set of duals of $R$ and $M$ and the set of linear maps of the set of Clifford algebras of $Q$ and the set of Clifford algebras of $Q$.

CliffordAlgebra.contractRightdefMathlib.LinearAlgebra.CliffordAlgebra.Contraction, function or constant

Wording

no wording

English

$\operatorname{contractRight}$ is a linear map of the set of Clifford algebras of $Q$ and the set of linear maps of the set of duals of $R$ and $M$ and the set of Clifford algebras of $Q$ defined as the flip of the complement of $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to $\operatorname{contractLeft}$ and the reverse and the reverse.

CliffordAlgebra.equivExteriordefMathlib.LinearAlgebra.CliffordAlgebra.Contraction, function or constant

Wording

the module isomorphism to the exterior algebra of Q (from the docstring)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the module isomorphism to the exterior algebra of $Q$ is a linear equivalence of the set of Clifford algebras of $Q$ and the set of exterior algebras of $R$ and $M$ defined as the change form equivalence of $\mathrm{CliffordAlgebra\_\_changeForm\_\_associated\_neg\_proof}$.

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

CliffordAlgebraComplex.QdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

no wording

English

$\operatorname{Q}$ is a quadratic form of $\Real$ and $\Real$ defined as $\operatorname{neg}$ applied to the square.

CliffordAlgebraComplex.equivdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an algebra isomorphism of the set of Clifford algebras of $\operatorname{Q}$ and the set of complexes defined as the algebra isomorphism of the complex and the Clifford algebra complex.

CliffordAlgebraComplex.ofComplexdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the Clifford algebra complex (from the name)

English

The Clifford algebra complex is an algebra homomorphism of the set of complexes and the set of Clifford algebras of $\operatorname{Q}$ defined as $\operatorname{lift}$ applied to $\mathrm{CliffordAlgebra\_\_\_u3b9\_\_\_app}$ applied to $\operatorname{Q}$ and $1$.

CliffordAlgebraComplex.toComplexdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the complex (from the name)

English

The complex is an algebra homomorphism of the set of Clifford algebras of $\operatorname{Q}$ and the set of complexes defined as $\operatorname{lift}$ applied to $\operatorname{Q}$ and the span singleton of $\operatorname{I}$.

CliffordAlgebraDualNumber.equivdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an algebra isomorphism of the set of Clifford algebras of $0$ and the set of dual numbers of $R$.

CliffordAlgebraQuaternion.QdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

no wording

English

Let $x_{1}$ and $x_{2}$ be elements of $R$. Then $\operatorname{Q}$ applied to $x_{1}$ and $x_{2}$ is a quadratic form of $R$ and $\mathrm{Prod}$ applied to $R$ and $R$ defined as the product of $\HSMulhSMulMACRoAL {x_{1}}{\operatorname{sq}}$ and $\HSMulhSMulMACRoAL {x_{2}}{\operatorname{sq}}$.

CliffordAlgebraQuaternion.equivdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an algebra isomorphism of the set of Clifford algebras of $\operatorname{Q}$ applied to $x_{1}$ and $x_{2}$ and the set of quaternion algebras of $0$ and $x_{2}$ defined as the algebra isomorphism of the quaternion and the Clifford algebra quaternion.

CliffordAlgebraQuaternion.ofQuaterniondefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the Clifford algebra quaternion (from the name)

English

The Clifford algebra quaternion is an algebra homomorphism of the set of quaternion algebras of $0$ and $x_{2}$ and the set of Clifford algebras of $\operatorname{Q}$ applied to $x_{1}$ and $x_{2}$ defined as the lift homomorphism of the quaternion basis of $x_{1}$ and $x_{2}$.

CliffordAlgebraQuaternion.quaternionBasisdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the quaternion basis of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be elements of $R$. Then the quaternion basis of $x_{1}$ and $x_{2}$ is a basis of $0$ and $x_{2}$.

CliffordAlgebraQuaternion.toQuaterniondefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the quaternion (from the name)

English

The quaternion is an algebra homomorphism of the set of Clifford algebras of $\operatorname{Q}$ applied to $x_{1}$ and $x_{2}$ and the set of quaternion algebras of $0$ and $x_{2}$.

CliffordAlgebraRing.equivdefMathlib.LinearAlgebra.CliffordAlgebra.Equivs, function or constant

Wording

the equivalence (from the name)

English

The equivalence is an algebra isomorphism of the set of Clifford algebras of $0$ and $R$.

Mathlib.LinearAlgebra.CliffordAlgebra.Even

CliffordAlgebra.EvenHomstructureMathlib.LinearAlgebra.CliffordAlgebra.Even, type

Wording

even homomorphism of Q and A (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $A$ be a set. Then the even homomorphisms of $Q$ and $A$ are a basic type.

CliffordAlgebra.EvenHom.bilindefMathlib.LinearAlgebra.CliffordAlgebra.Even, function or constant

Wording

the bilinear of self (from the name)

English

Let $\mathrm{self}$ be an even homomorphism of $Q$ and $A$. Then the bilinear of $\mathrm{self}$ is a linear map of $M$ and the set of linear maps of $M$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

CliffordAlgebra.EvenHom.compr₂defMathlib.LinearAlgebra.CliffordAlgebra.Even, function or constant

Wording

no wording

English

Let $g$ be an even homomorphism of $Q$ and $A$. Let $f$ be an algebra homomorphism of $A$ and $B$. Then $\mathrm{CliffordAlgebra\_\_EvenHom\_\_compr\_u2082\_}$ applied to $g$ and $f$ is an even homomorphism of $Q$ and $B$.

CliffordAlgebra.evendefMathlib.LinearAlgebra.CliffordAlgebra.Even, function or constant

Wording

the even submodule of Q (from the docstring)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the even submodule of $Q$ is a subalgebra of $R$ and the set of Clifford algebras of $Q$.

CliffordAlgebra.even.liftdefMathlib.LinearAlgebra.CliffordAlgebra.Even, function or constant

Wording

the lift of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the lift of $Q$ is an element of $\EquivMACRoAE {\operatorname{EvenHom} (Q , A)}{\mathrm{AlgHom} (\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{even} (Q)}{x_{5}})}, A)}$.

CliffordAlgebra.even.ιdefMathlib.LinearAlgebra.CliffordAlgebra.Even, function or constant

Wording

the inclusion of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the inclusion of $Q$ is an even homomorphism of $Q$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (Q)}{x_{3}})}$.

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

CliffordAlgebra.EquivEven.Q'defMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Then $\operatorname{Q'}$ applied to $Q$ is a quadratic form of $R$ and $\mathrm{Prod}$ applied to $M$ and $R$ defined as the product of $Q$ and $\operatorname{neg}$ applied to the square.

CliffordAlgebra.EquivEven.e0defMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Then $\operatorname{e0}$ applied to $Q$ is a Clifford algebra of $\operatorname{Q'}$ applied to $Q$ defined as $\mathrm{CliffordAlgebra\_\_\_u3b9\_\_\_app}$ applied to $\operatorname{Q'}$ applied to $Q$ and $\ProdmkMACRoU {0}{1}$.

CliffordAlgebra.EquivEven.vdefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Then $\operatorname{v}$ applied to $Q$ is a linear map of $M$ and the set of Clifford algebras of $\operatorname{Q'}$ applied to $Q$ defined as the composition of the inclusion of $\operatorname{Q'}$ applied to $Q$ and the left injection of $M$ and $R$.

CliffordAlgebra.equivEvendefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

the equivalence even of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the equivalence even of $Q$ is an algebra isomorphism of the set of Clifford algebras of $Q$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (\operatorname{Q'} (Q))}{x_{3}})}$ defined as the algebra isomorphism of the even of $Q$ and the Clifford algebra of $Q$.

CliffordAlgebra.evenEquivEvenNegdefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

the even equivalence even negation of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the even equivalence even negation of $Q$ is an algebra isomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (Q)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{even} (\operatorname{neg} (Q))}{x_{4}})}$.

CliffordAlgebra.evenToNegdefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

the even to negation of Q and h (from the name)

English

Let $Q$ and $\mathrm{Q'}$ be quadratic forms of $R$ and $M$ such that $\EqtMACRoH {\mathrm{Q'}}{\operatorname{neg} (Q)}$. Then the even to negation of $Q$ and $\mathrm{Q'}$ is an algebra homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (Q)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{even} (\mathrm{Q'})}{x_{4}})}$.

CliffordAlgebra.ofEvendefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

the Clifford algebra of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the Clifford algebra of $Q$ is an algebra homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (\operatorname{Q'} (Q))}{x_{3}})}$ and the set of Clifford algebras of $Q$.

CliffordAlgebra.toEvendefMathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv, function or constant

Wording

the even of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the even of $Q$ is an algebra homomorphism of the set of Clifford algebras of $Q$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{even} (\operatorname{Q'} (Q))}{x_{3}})}$.

Mathlib.LinearAlgebra.CliffordAlgebra.Fold

CliffordAlgebra.foldldefMathlib.LinearAlgebra.CliffordAlgebra.Fold, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $N$ such that for all elements $m$ of $M$, for all elements $x_{5}$ of $N$, $\EqtMACRoH {\operatorname{coe} (f , m , \operatorname{coe} (f , m , x_{5}))}{\HSMulhSMulMACRoAL {Q (m)}{x_{5}}}$. Then $\operatorname{foldl}$ applied to $Q$, $f$ and $\mathrm{hf}$ is a linear map of $N$ and the set of linear maps of the set of Clifford algebras of $Q$ and $N$ defined as the complement of $\operatorname{foldr}$ applied to $Q$, $f$ and $\mathrm{hf}$ and the reverse.

CliffordAlgebra.foldrdefMathlib.LinearAlgebra.CliffordAlgebra.Fold, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $N$ such that for all elements $m$ of $M$, for all elements $x_{5}$ of $N$, $\EqtMACRoH {\operatorname{coe} (f , m , \operatorname{coe} (f , m , x_{5}))}{\HSMulhSMulMACRoAL {Q (m)}{x_{5}}}$. Then $\operatorname{foldr}$ applied to $Q$, $f$ and $\mathrm{hf}$ is a linear map of $N$ and the set of linear maps of the set of Clifford algebras of $Q$ and $N$ defined as the flip of the linear map of $\operatorname{lift}$ applied to $Q$ and $f$.

CliffordAlgebra.foldr'defMathlib.LinearAlgebra.CliffordAlgebra.Fold, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $f$ be a linear map of $M$ and the set of linear maps of $\mathrm{Prod}$ applied to the set of Clifford algebras of $Q$ and $N$ and $N$ such that for all elements $m$ of $M$, for all Clifford algebras $x_{5}$ of $Q$, for all elements $\mathrm{fx}$ of $N$, $\EqtMACRoH {\operatorname{coe} (f , m , \ProdmkMACRoU {(\mathrm{CliffordAlgebra\_\_\_u3b9\_\_\_app} (Q , m)\times x_{5})}{\operatorname{coe} (f , m , \ProdmkMACRoU {x_{5}}{\mathrm{fx}})})}{\HSMulhSMulMACRoAL {Q (m)}{\mathrm{fx}}}$. Let $n$ be an element of $N$. Then $\operatorname{foldr'}$ applied to $Q$, $f$, $\mathrm{hf}$ and $n$ is a linear map of the set of Clifford algebras of $Q$ and $N$ defined as the composition of the second component of the set of Clifford algebras of $Q$ and $N$ and $\operatorname{foldr}$ applied to $Q$, $\operatorname{foldr'Aux}$ applied to $Q$ and $f$, $\mathrm{CliffordAlgebra\_\_foldr'Aux\_foldr'Aux}$ applied to $Q$, $f$ and $\mathrm{hf}$ and $\ProdmkMACRoU {1}{n}$.

Mathlib.LinearAlgebra.CliffordAlgebra.Grading

CliffordAlgebra.GradedAlgebra.ιdefMathlib.LinearAlgebra.CliffordAlgebra.Grading, function or constant

Wording

the inclusion of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the inclusion of $Q$ is a linear map of $M$ and the set of direct sums of $\mathrm{ZMod}$ applied to $2$ and the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{evenOdd} (Q , i)}{x_{3}})}$ defined as the composition of $\operatorname{lof}$ applied to $R$, $\mathrm{ZMod}$ applied to $2$, the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{evenOdd} (Q , i)}{x_{3}})}$ and $1$ and $\operatorname{codRestrict}$ applied to $\operatorname{evenOdd}$ applied to $Q$ and $1$, the inclusion of $Q$ and $\mathrm{CliffordAlgebra\_\_\_u3b9\_\_mem\_evenOdd\_one}$ applied to $Q$.

CliffordAlgebra.evenOdddefMathlib.LinearAlgebra.CliffordAlgebra.Grading, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Let $i$ be an element of $\mathrm{ZMod}$ applied to $2$. Then $\operatorname{evenOdd}$ applied to $Q$ and $i$ is a submodule of $R$ and the set of Clifford algebras of $Q$ defined as the supremum of the function that maps $j$ to the exponentiation of the range of the inclusion of $Q$ to $j$.

Mathlib.LinearAlgebra.CliffordAlgebra.Prod

CliffordAlgebra.ofProddefMathlib.LinearAlgebra.CliffordAlgebra.Prod, function or constant

Wording

the Clifford algebra of x7 and x8 (from the name)

English

Let $x_{7}$ be a quadratic form of $R$ and $x$. Let $x_{8}$ be a quadratic form of $R$ and $x_{1}$. Then the Clifford algebra of $x_{7}$ and $x_{8}$ is an algebra homomorphism of the set of Clifford algebras of the product of $x_{7}$ and $x_{8}$ and the set of graded tensor products of $\operatorname{evenOdd}$ applied to $x_{7}$ and $\operatorname{evenOdd}$ applied to $x_{8}$ defined as $\operatorname{lift}$ applied to the product of $x_{7}$ and $x_{8}$ and the coprod function of the composition of the linear map of $\operatorname{includeLeft}$ applied to $\operatorname{evenOdd}$ applied to $x_{7}$ and $\operatorname{evenOdd}$ applied to $x_{8}$ and the composition of the subtype of $\operatorname{evenOdd}$ applied to $x_{7}$ and $1$ and $\operatorname{codRestrict}$ applied to $\operatorname{evenOdd}$ applied to $x_{7}$ and $1$, the inclusion of $x_{7}$ and $\mathrm{CliffordAlgebra\_\_\_u3b9\_\_mem\_evenOdd\_one}$ applied to $x_{7}$ and the composition of the linear map of $\operatorname{includeRight}$ applied to $\operatorname{evenOdd}$ applied to $x_{7}$ and $\operatorname{evenOdd}$ applied to $x_{8}$ and the composition of the subtype of $\operatorname{evenOdd}$ applied to $x_{8}$ and $1$ and $\operatorname{codRestrict}$ applied to $\operatorname{evenOdd}$ applied to $x_{8}$ and $1$, the inclusion of $x_{8}$ and $\mathrm{CliffordAlgebra\_\_\_u3b9\_\_mem\_evenOdd\_one}$ applied to $x_{8}$.

CliffordAlgebra.prodEquivdefMathlib.LinearAlgebra.CliffordAlgebra.Prod, function or constant

Wording

the product equivalence of x7 and x8 (from the name)

English

Let $x_{7}$ be a quadratic form of $R$ and $x$. Let $x_{8}$ be a quadratic form of $R$ and $x_{1}$. Then the product equivalence of $x_{7}$ and $x_{8}$ is an algebra isomorphism of the set of Clifford algebras of the product of $x_{7}$ and $x_{8}$ and the set of graded tensor products of $\operatorname{evenOdd}$ applied to $x_{7}$ and $\operatorname{evenOdd}$ applied to $x_{8}$ defined as the algebra isomorphism of the Clifford algebra of $x_{7}$ and $x_{8}$ and the product of $x_{7}$ and $x_{8}$.

CliffordAlgebra.toProddefMathlib.LinearAlgebra.CliffordAlgebra.Prod, function or constant

Wording

the product of x7 and x8 (from the name)

English

Let $x_{7}$ be a quadratic form of $R$ and $x$. Let $x_{8}$ be a quadratic form of $R$ and $x_{1}$. Then the product of $x_{7}$ and $x_{8}$ is an algebra homomorphism of the set of graded tensor products of $\operatorname{evenOdd}$ applied to $x_{7}$ and $\operatorname{evenOdd}$ applied to $x_{8}$ and the set of Clifford algebras of the product of $x_{7}$ and $x_{8}$.

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

lipschitzGroupdefMathlib.LinearAlgebra.CliffordAlgebra.SpinGroup, function or constant

Wording

the Lipschitz group of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the Lipschitz group of $Q$ is a subgroup of the set of units of the set of Clifford algebras of $Q$ defined as the closure of the preimage of $\operatorname{val}$ and the range of $\operatorname{coe}$ applied to the inclusion of $Q$.

pinGroupdefMathlib.LinearAlgebra.CliffordAlgebra.SpinGroup, function or constant

Wording

no wording

English

Let $Q$ be a quadratic form of $R$ and $M$. Then $\mathrm{pinGroup}$ applied to $Q$ is a submonoid of the set of Clifford algebras of $Q$ defined as the minimum of the map of the coercion homomorphism of the set of Clifford algebras of $Q$ and $\operatorname{toSubmonoid}$ applied to the Lipschitz group of $Q$ and $\mathrm{unitary}$ applied to the set of Clifford algebras of $Q$.

pinGroup.toUnitsdefMathlib.LinearAlgebra.CliffordAlgebra.SpinGroup, function or constant

Wording

the unit (from the name)

English

The unit is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{pinGroup} (Q)}{x_{3}})}$ and the set of units of the set of Clifford algebras of $Q$.

spinGroupdefMathlib.LinearAlgebra.CliffordAlgebra.SpinGroup, function or constant

Wording

the spin group of Q (from the name)

English

Let $Q$ be a quadratic form of $R$ and $M$. Then the spin group of $Q$ is a submonoid of the set of Clifford algebras of $Q$ defined as the minimum of $\mathrm{pinGroup}$ applied to $Q$ and $\operatorname{toSubmonoid}$ applied to $\operatorname{toSubsemiring}$ applied to the subring of the even submodule of $Q$.

spinGroup.toUnitsdefMathlib.LinearAlgebra.CliffordAlgebra.SpinGroup, function or constant

Wording

the unit (from the name)

English

The unit is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{spinGroup} (Q)}{x_{3}})}$ and $\UnitsMACRoAO {\mathrm{CliffordAlgebra} (Q)}$.

Mathlib.LinearAlgebra.Coevaluation

coevaluationdefMathlib.LinearAlgebra.Coevaluation, function or constant

Wording

the coevaluation map of K and V (from the docstring)

English

Let $K$ and $V$ be sets. Then the coevaluation map of $K$ and $V$ is a linear map of $K$ and the set of tensor products of $V$ and the set of duals of $K$ and $V$ defined as $\operatorname{constr}$ applied to the singleton of $\mathrm{Unit}$ and $K$, $K$ and the function that maps $x_{4}$ to $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{tmul} (K , \operatorname{ofVectorSpace} (K , V , i), \operatorname{coord} (\operatorname{ofVectorSpace} (K , V), i))}$.

Mathlib.LinearAlgebra.Complex.Module

Complex.basisOneIdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the basis one (from the name)

English

The basis one is a basis of $\Real$ and the set of complexes.

Complex.conjAedefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

no wording

English

$\operatorname{conjAe}$ is an algebra isomorphism of the set of complexes and the set of complexes.

Complex.equivRealProdLmdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

no wording

English

$\operatorname{equivRealProdLm}$ is a linear equivalence of the set of complexes and $\mathrm{Prod}$ applied to $\Real$ and $\Real$.

Complex.imLmdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

no wording

English

$\operatorname{imLm}$ is a linear map of the set of complexes and $\Real$.

Complex.liftdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the lift (from the name)

English

The lift is an equivalence from $\SubtypeSet {\mathrm{I'}}{(\EqtMACRoH {(\mathrm{I'} \times \mathrm{I'})}{\operatorname{neg} (1)})}$ to the set of algebra homomorphisms of the set of complexes and $A$.

Complex.ofRealAmdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the complex (from the name)

English

The complex is an algebra homomorphism of $\Real$ and the set of complexes defined as the algebra of $\Real$ and the set of complexes.

Complex.reLmdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

no wording

English

$\operatorname{reLm}$ is a linear map of the set of complexes and $\Real$.

Complex.selfAdjointEquivdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the self adjoint equivalence (from the name)

English

The self adjoint equivalence is a linear equivalence of $\SubtypeSet {x}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (\mathrm{Complex})}{x})}$ and $\Real$.

imaginaryPartdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the imaginary part (from the docstring)

English

The imaginary part is a linear map of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{3}})}$ defined as the composition of $\operatorname{negISMul}$ and the skew adjoint part of $\Real$.

realPartdefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

the real part (from the docstring)

English

The real part is a linear map of $A$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{3}})}$ defined as the self-adjoint part of $\Real$.

skewAdjoint.negISMuldefMathlib.LinearAlgebra.Complex.Module, function or constant

Wording

no wording

English

$\operatorname{negISMul}$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{skewAdjoint} (A)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{selfAdjoint} (A)}{x_{4}})}$.

Mathlib.LinearAlgebra.Complex.Orientation

Complex.orientationdefMathlib.LinearAlgebra.Complex.Orientation, function or constant

Wording

the orientation (from the name)

English

The orientation is an orientation of the set of complexes and $\mathrm{Fin}$ applied to $2$ defined as the orientation of the basis one.

Mathlib.LinearAlgebra.Contraction

TensorProduct.dualDistribEquivdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

the dual distributive equivalence of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the dual distributive equivalence of $M$ and $N$ is a linear equivalence of the set of tensor products of the set of duals of $R$ and $M$ and the set of duals of $R$ and $N$ and the set of duals of $R$ and the set of tensor products of $M$ and $N$ defined as the composition of the homomorphism tensor homomorphism equivalence of $R$ and $R$ and the right congruence of $\operatorname{rid}$ applied to $R$ and $R$.

contractLeftdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{contractLeft}$ applied to $R$ and $M$ is a linear map of the set of tensor products of the set of duals of $R$ and $M$ and $M$ and $R$ defined as the additive homomorphism of $\operatorname{toAddHom}$ applied to $\operatorname{uncurry}$ applied to the identity ring homomorphism of $R$, the set of duals of $R$ and $M$, $M$ and $R$ and the identity.

contractRightdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\mathrm{contractRight}$ applied to $R$ and $M$ is a linear map of the set of tensor products of $M$ and the set of duals of $R$ and $M$ and $R$ defined as the additive homomorphism of $\operatorname{toAddHom}$ applied to $\operatorname{uncurry}$ applied to the identity ring homomorphism of $R$, $M$, the set of duals of $R$ and $M$ and $R$ and the flip of the identity.

dualTensorHomdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

the dual tensor homomorphism of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the dual tensor homomorphism of $M$ and $N$ is a linear map of the set of tensor products of the set of duals of $R$ and $M$ and $N$ and the set of linear maps of $M$ and $N$ defined as $\operatorname{uncurry}$ applied to the identity ring homomorphism of $R$, the set of duals of $R$ and $M$, $N$, the set of linear maps of $M$ and $N$ and the right scalar multiple.

dualTensorHomEquivdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

the dual tensor homomorphism equivalence of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the dual tensor homomorphism equivalence of $M$ and $N$ is a linear equivalence of the set of tensor products of the set of duals of $R$ and $M$ and $N$ and the set of linear maps of $M$ and $N$ defined as the linear equivalence of the dual tensor homomorphism of $M$ and $N$ and $\mathrm{dualTensorHom\_bijective}$.

dualTensorHomEquivOfBasisdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

the dual tensor homomorphism equivalence of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the dual tensor homomorphism equivalence of $b$ is a linear equivalence of the set of tensor products of the set of duals of $R$ and $M$ and $N$ and the set of linear maps of $M$ and $N$.

homTensorHomEquivdefMathlib.LinearAlgebra.Contraction, function or constant

Wording

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

English

Let $R$, $M$, $N$, $P$ and $Q$ be sets. Then the homomorphism tensor homomorphism equivalence of $P$ and $Q$ is a linear equivalence 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$.

lTensorHomEquivHomLTensordefMathlib.LinearAlgebra.Contraction, function or constant

Wording

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

English

Let $R$, $M$, $P$ and $Q$ be sets. Then the tensor homomorphism equivalence homomorphism tensor of $P$ and $Q$ is a linear equivalence of the set of tensor products of $P$ and the set of linear maps of $M$ and $Q$ and the set of linear maps of $M$ and the set of tensor products of $P$ and $Q$ defined as the composition of the composition of the congruence of the identity map of $R$ and $P$ and the inverse of the dual tensor homomorphism equivalence of $M$ and $Q$ and $\operatorname{leftComm}$ applied to $R$, $P$, the set of duals of $R$ and $M$ and $Q$ and the dual tensor homomorphism equivalence of $M$ and the set of tensor products of $P$ and $Q$.

rTensorHomEquivHomRTensordefMathlib.LinearAlgebra.Contraction, function or constant

Wording

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

English

Let $R$, $M$, $P$ and $Q$ be sets. Then the tensor homomorphism equivalence homomorphism tensor of $P$ and $Q$ is a linear equivalence of the set of tensor products of the set of linear maps of $M$ and $P$ and $Q$ and the set of linear maps of $M$ and the set of tensor products of $P$ and $Q$ defined as the composition of the composition of the congruence of the inverse of the dual tensor homomorphism equivalence of $M$ and $P$ and the identity map of $R$ and $Q$ and the associator of $P$ and $Q$ and the dual tensor homomorphism equivalence of $M$ and the set of tensor products of $P$ and $Q$.

Mathlib.LinearAlgebra.CrossProduct

crossProductdefMathlib.LinearAlgebra.CrossProduct, function or constant

Wording

the cross product (from the name)

English

The cross product is a linear map of the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$ and the set of linear maps of the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to $3$ to elements of $R$.

Mathlib.LinearAlgebra.DFinsupp

DFinsupp.coprodMapdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the coproduct map of f (from the name)

English

Let $f$ be a function from elements $i_{1}$ of $x$ to linear maps of $M$ applied to $i_{1}$ and $N$. Then the coproduct map of $i_{1}$ is a linear map of the set of finitely supported functions of the function that maps $i$ to $M$ applied to $i$ and $N$ defined as the function that maps $f$ to the composition of $\operatorname{lsum}$ applied to $\Natural$ and the function that maps $x_{8}$ to the identity and the linear map of $i_{1}$.

DFinsupp.domLCongrdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the domain congruence of e (from the name)

English

Let $e$ be an equivalence from $x$ to $x_{1}$. Then the domain congruence of $e$ is a linear equivalence of the set of finitely supported functions of the function that maps $i$ to $M$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $\operatorname{symm}$ applied to $e$ and $i_{1}$.

DFinsupp.lapplydefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\operatorname{lapply}$ applied to $i$ is a linear map of the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $M$ applied to $i$.

DFinsupp.linearEquivFunOnFintypedefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the linear equivalence function on finite type (from the name)

English

The linear equivalence function on finite type is a linear equivalence of the set of finitely supported functions of the function that maps $i$ to $M$ applied to $i$ and the set of functions from elements $i_{1}$ of $x$ to elements of $M$ applied to $i_{1}$.

DFinsupp.lmkdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x$. Then $\operatorname{lmk}$ applied to $s$ is a linear map of the set of functions from elements $i$ of $s$ to elements of $M$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $i_{1}$.

DFinsupp.lsingledefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

no wording

English

Let $i$ be an element of $x$. Then $\operatorname{lsingle}$ applied to $i$ is a linear map of $M$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $i_{1}$.

DFinsupp.lsumdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

no wording

English

Let $S$ be a set. Then $\operatorname{lsum}$ applied to $S$ is a linear equivalence of the set of functions from elements $i$ of $x$ to linear maps of $M$ applied to $i$ and $N$ and the set of linear maps of the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and $N$.

DFinsupp.mapRange.linearEquivdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the linear equivalence of e (from the name)

English

Let $e$ be a function from elements $i_{2}$ of $x$ to linear equivalences of $x_{2}$ applied to $i_{2}$ and $x_{3}$ applied to $i_{2}$. Then the linear equivalence of $i_{2}$ is a linear equivalence of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{3}$ applied to $i_{1}$.

DFinsupp.mapRange.linearMapdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the linear map of f (from the name)

English

Let $f$ be a function from elements $i_{2}$ of $x$ to linear maps of $x_{2}$ applied to $i_{2}$ and $x_{3}$ applied to $i_{2}$. Then the linear map of $i_{2}$ is a linear map of the set of finitely supported functions of the function that maps $i$ to $x_{2}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to $x_{3}$ applied to $i_{1}$.

DFinsupp.sigmaCurryLEquivdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the sigma curry equivalence (from the name)

English

The sigma curry equivalence is a linear equivalence of the set of finitely supported functions of the function that maps $i$ to $M$ applied to $\operatorname{fst}$ applied to $i$ and $\operatorname{snd}$ applied to $i$ and the set of finitely supported functions of the function that maps $i_{1}$ to the set of finitely supported functions of the function that maps $j$ to $M$ applied to $i_{1}$ and $j$.

iSupIndep.linearEquivdefMathlib.LinearAlgebra.DFinsupp, function or constant

Wording

the linear equivalence of ind and iSup_top (from the name)

English

Assume that $\mathrm{iSupIndep}$ holds for $p$. Assume that the supremum of the function that maps $i_{1}$ to $p$ applied to $i_{1}$ is equal to the top. Then the linear equivalence of $\mathrm{ind}$ and $\mathrm{iSup\_top}$ is a linear equivalence of the set of finitely supported functions of the function that maps $i$ to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p (i)}{x_{5}})}$ and $N$.

Mathlib.LinearAlgebra.Determinant

LinearEquiv.detdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the determinant (from the name)

English

The determinant is a monoid homomorphism of the set of linear equivalences of $M$ and $M$ and $\UnitsMACRoAO {R}$ defined as the composition of the map of the determinant and the monoid homomorphism of the inverse of the general linear group on $R$ and $M$.

LinearEquiv.ofIsUnitDetdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the linear equivalence of h (from the name)

English

Assume that the determinant of $\operatorname{toMatrix}$ applied to $v$, $\mathrm{v'}$ and $f$ is a unit. Then the linear equivalence of $h$ is a linear equivalence of $M$ and $\mathrm{M'}$.

LinearMap.detdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the determinant (from the docstring)

English

The determinant is a monoid homomorphism of the set of linear maps of $M$ and $M$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{LinearMap\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_Determinant\_\_1959956828\_\_\_hygCtx\_\_\_hyg\_\_8}$.

LinearMap.equivOfDetNeZerodefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the equivalence of f and hf (from the name)

English

Let $f$ be a linear map of $M$ and $M$ such that $\operatorname{det} (f)\neq 0$. Then the equivalence of $f$ and $\mathrm{hf}$ is a linear equivalence of $M$ and $M$.

LinearMap.equivOfIsUnitDetdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the equivalence of h2 (from the name)

English

Assume that $\operatorname{det}$ applied to $f$ is a unit. Then the equivalence of $h_{2}$ is a linear equivalence of $M$ and $M$.

Matrix.indexEquivOfInvdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the index equivalence of #1 and #2 (from the name)

English

Assume that $\EqtMACRoH {M \times \mathrm{M'}}{1}$. Assume that $\EqtMACRoH {\mathrm{M'} \times M}{1}$. Then the index equivalence of $\mathrm{hMM'}$ and $\mathrm{hM'M}$ is an equivalence from $m$ to $n$ defined as the equivalence of $\operatorname{toLin'OfInv}$ applied to $\mathrm{hMM'}$ and $\mathrm{hM'M}$.

Module.Basis.detdefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the determinant of e (from the docstring)

English

Let $e$ be a basis of $R$ and $M$. Then the determinant of $e$ is an alternating map of $R$ and $x_{3}$.

equivOfPiLEquivPidefMathlib.LinearAlgebra.Determinant, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be a linear equivalence of the set of functions from elements of $m$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$. Then the equivalence of $e$ is an equivalence from $m$ to $n$ defined as the index equivalence of the basis of the inverse of $e$ and the basis function of $R$ and $n$.

Mathlib.LinearAlgebra.Dimension.Basic

Module.rankdefMathlib.LinearAlgebra.Dimension.Basic, function or constant

Wording

the rank of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the rank of $R$ and $M$ is a cardinal defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_Dimension\_\_Basic\_\_3070247278\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$ and $M$.

Mathlib.LinearAlgebra.Dimension.Constructions

Module.Basis.sumQuotdefMathlib.LinearAlgebra.Dimension.Constructions, function or constant

Wording

the sum quotient of bW and bQ (from the name)

English

Let $\mathrm{bW}$ be a basis of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$. Let $\mathrm{bQ}$ be a basis of $R$ and the set of quotients of $V$ and $W$. Then the sum quotient of $\mathrm{bW}$ and $\mathrm{bQ}$ is a basis of $R$ and $V$.

Set.finrankdefMathlib.LinearAlgebra.Dimension.Constructions, function or constant

Wording

the rank of R and s (from the docstring)

English

Let $R$ be a set. Let $s$ be an element of $\wp M$. Then the rank of $R$ and $s$ is an element of $\Natural$ defined as the rank of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{span} (R , s)}{x_{3}})}$.

finDimVectorspaceEquivdefMathlib.LinearAlgebra.Dimension.Constructions, function or constant

Wording

no wording

English

Let $n$ be a natural number such that the rank of $R$ and $M$ is equal to $n$. Then $\mathrm{finDimVectorspaceEquiv}$ applied to $n$ and $\mathrm{hn}$ is a linear equivalence of $M$ and the set of functions from elements of $\mathrm{Fin}$ applied to $n$ to elements of $R$.

Mathlib.LinearAlgebra.Dimension.Finrank

Module.finrankdefMathlib.LinearAlgebra.Dimension.Finrank, function or constant

Wording

the rank of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the rank of $R$ and $M$ is a natural number defined as $\operatorname{toNat}$ applied to the rank of $R$ and $M$.

Mathlib.LinearAlgebra.Dimension.Free

LinearEquiv.ofFinrankEqdefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the linear equivalence of cond and #3 (from the name)

English

Let $M$ and $\mathrm{M'}$ be sets such that the rank of $R$ and $M$ is equal to the rank of $R$ and $\mathrm{M'}$. Then the linear equivalence of $\mathrm{M'}$ and $\mathrm{cond}$ is a linear equivalence of $M$ and $\mathrm{M'}$ defined as $\operatorname{choice}$ applied to $\mathrm{FiniteDimensional\_\_nonempty\_linearEquiv\_of\_finrank\_eq}$ applied to $\mathrm{cond}$.

LinearEquiv.ofLiftRankEqdefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the linear equivalence of cond and #3 (from the name)

English

Let $M$ and $\mathrm{M'}$ be sets such that the lift of the rank of $R$ and $M$ is equal to the lift of the rank of $R$ and $\mathrm{M'}$. Then the linear equivalence of $\mathrm{M'}$ and $\mathrm{cond}$ is a linear equivalence of $M$ and $\mathrm{M'}$ defined as $\operatorname{choice}$ applied to $\mathrm{nonempty\_linearEquiv\_of\_lift\_rank\_eq}$ applied to $\mathrm{cond}$.

LinearEquiv.ofRankEqdefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the linear equivalence of x and cond (from the name)

English

Let $M$ and $x$ be sets such that the rank of $R$ and $M$ is equal to the rank of $R$ and $x$. Then the linear equivalence of $x$ and $\mathrm{cond}$ is a linear equivalence of $M$ and $x$ defined as $\operatorname{choice}$ applied to $\mathrm{nonempty\_linearEquiv\_of\_rank\_eq}$ applied to $\mathrm{cond}$.

LinearEquiv.smul_id_of_finrank_eq_onedefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the scalar multiple identity of d1 (from the name)

English

Assume that the rank of $R$ and $M$ is equal to $1$. Then the scalar multiple identity of $d_{1}$ is a linear equivalence of $R$ and the set of linear maps of $M$ and $M$.

Module.basisUniquedefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

no wording

English

Let $x_{3}$ be a set. Assume that the rank of $R$ and $M$ is equal to $1$. Then $\operatorname{basisUnique}$ applied to $x_{3}$ and $h_{2}$ is a basis of $R$ and $M$ defined as the reindexing of the finite basis of $M$ and $h_{2}$ and the equivalence of $\mathrm{Fin}$ applied to $1$ and $x_{3}$.

Module.finBasisdefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the finite basis of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the finite basis of $R$ and $M$ is a basis of $R$ and $M$.

Module.finBasisOfFinrankEqdefMathlib.LinearAlgebra.Dimension.Free, function or constant

Wording

the finite basis of M and hn (from the name)

English

Let $R$ and $M$ be sets such that the rank of $R$ and $M$ is equal to $n$. Then the finite basis of $M$ and $\mathrm{hn}$ is a basis of $R$ and $M$ defined as the reindexing of the finite basis of $R$ and $M$ and the finite congruence of $\mathrm{hn}$.

Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Basis.ofRankEqZerodefMathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition, function or constant

Wording

the basis of hV (from the name)

English

Assume that the rank of $K$ and $V$ is equal to $0$. Then the basis of $\mathrm{hV}$ is a basis of $K$ and $V$ defined as $\operatorname{empty}$ applied to $V$.

Mathlib.LinearAlgebra.Dimension.LinearMap

LinearMap.rankdefMathlib.LinearAlgebra.Dimension.LinearMap, function or constant

Wording

the rank of f (from the name)

English

Let $f$ be a linear map of $V$ and $\mathrm{V'}$. Then the rank of $f$ is a cardinal defined as the rank of $K$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

Mathlib.LinearAlgebra.Dimension.OrzechProperty

basisOfTopLeSpanOfCardEqFinrankdefMathlib.LinearAlgebra.Dimension.OrzechProperty, function or constant

Wording

the basis of b (from the name)

English

Let $b$ be a function from elements of $x_{3}$ to elements of $M$ such that the top is less than or equal to the span of $R$ and the range of $b$. Assume that the cardinality of $x_{3}$ is equal to the rank of $R$ and $M$. Then the basis of $b$ is a basis of $R$ and $M$ defined as $\operatorname{mk}$ applied to $\mathrm{linearIndependent\_of\_top\_le\_span\_of\_card\_eq\_finrank}$ applied to $\mathrm{le\_span}$ and $\mathrm{card\_eq}$ and $\mathrm{le\_span}$.

finsetBasisOfTopLeSpanOfCardEqFinrankdefMathlib.LinearAlgebra.Dimension.OrzechProperty, function or constant

Wording

the finite set basis of le_span and card_eq (from the name)

English

Assume that the top is less than or equal to the span of $R$ and $s$. Assume that the cardinality of $s$ is equal to the rank of $R$ and $M$. Then the finite set basis of $\mathrm{le\_span}$ and $\mathrm{card\_eq}$ is a basis of $R$ and $M$.

setBasisOfTopLeSpanOfCardEqFinrankdefMathlib.LinearAlgebra.Dimension.OrzechProperty, function or constant

Wording

the set basis of le_span and card_eq (from the name)

English

Assume that the top is less than or equal to the span of $R$ and $s$. Assume that the cardinality of the finite set of $s$ is equal to the rank of $R$ and $M$. Then the set basis of $\mathrm{le\_span}$ and $\mathrm{card\_eq}$ is a basis of $R$ and $M$.

Mathlib.LinearAlgebra.Dimension.RankNullity

HasRankNullityclassMathlib.LinearAlgebra.Dimension.RankNullity, predicate

Wording

no wording

English

Let $R$ be a set. Then we can say that $\mathrm{HasRankNullity}$ holds for $R$.

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Algebra.IsQuadraticExtensionclassMathlib.LinearAlgebra.Dimension.StrongRankCondition, predicate

Wording

no wording

English

Let $R$ and $S$ be sets. Then we can say that $\operatorname{IsQuadraticExtension}$ holds for $R$ and $S$.

Module.Basis.indexEquivdefMathlib.LinearAlgebra.Dimension.StrongRankCondition, function or constant

Wording

the index equivalence of v and #2 (from the name)

English

Let $v$ and $\mathrm{v'}$ be bases of $R$ and $M$. Then the index equivalence of $v$ and $\mathrm{v'}$ is an equivalence from $x_{3}$ to $x_{4}$.

Submodule.inductionOnRankdefMathlib.LinearAlgebra.Dimension.StrongRankCondition, function or constant

Wording

the induction on rank of ih and N1 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $P$ be a function from submodules of $R$ and $M$ to sets. Let $\mathrm{ih}$ be a function from submodules $N_{1}$ of $R$ and $M$ and functions from submodules $\mathrm{N'}$ of $R$ and $M$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Leq} (\mathrm{N'} , N_{1})$ and elements $x_{5}$ of $M$ and elements of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {N_{1}}{x_{5}}$ and elements of $\mathrm{Proof}$ applied to the proposition that for all elements $c$ of $R$, for all elements $y$ of $M$, if $y$ is an element of $\mathrm{N'}$, then if $\EqtMACRoH {\HSMulhSMulMACRoAL {c}{x_{5}}+ y}{0}$, then $\EqtMACRoH {c}{0}$ to elements of $P$ applied to $\mathrm{N'}$ to elements of $P$ applied to $N_{1}$. Let $N$ be a submodule of $R$ and $M$. Then the induction on rank of $N_{1}$ and $\mathrm{ih}$ is an element of $P$ applied to $N$.

Mathlib.LinearAlgebra.DirectSum.Finsupp

TensorProduct.finsuppLeftdefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the left finitely supported function of N and x8 (from the name)

English

Let $R$, $S$, $M$, $N$ and $x_{8}$ be sets. Then the left finitely supported function of $N$ and $x_{8}$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x_{8}}{M}$ and $N$ and the set of finitely supported functions from $x_{8}$ to the set of tensor products of $M$ and $N$ defined as the composition of the composition of the congruence of the finitely supported function equivalence direct sum of $M$ and $x_{8}$ and the identity map of $R$ and $N$ and the left direct sum of the function that maps $x_{10}$ to $M$ and the inverse of the finitely supported function equivalence direct sum of the set of tensor products of $M$ and $N$ and $x_{8}$.

TensorProduct.finsuppRightdefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the right finitely supported function of N and x8 (from the name)

English

Let $R$, $S$, $M$, $N$ and $x_{8}$ be sets. Then the right finitely supported function of $N$ and $x_{8}$ is a linear equivalence of the set of tensor products of $M$ and $\FinsuppMACRoQ {x_{8}}{N}$ and the set of finitely supported functions from $x_{8}$ to the set of tensor products of $M$ and $N$ defined as the composition of the composition of the congruence of the identity map of $S$ and $M$ and the finitely supported function equivalence direct sum of $N$ and $x_{8}$ and the right direct sum of the function that maps $x_{10}$ to $N$ and the inverse of the finitely supported function equivalence direct sum of the set of tensor products of $M$ and $N$ and $x_{8}$.

TensorProduct.finsuppScalarLeftdefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the left finitely supported function scalar of N and x3 (from the name)

English

Let $R$, $N$ and $x_{3}$ be sets. Then the left finitely supported function scalar of $N$ and $x_{3}$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x_{3}}{R}$ and $N$ and $\FinsuppMACRoQ {x_{3}}{N}$ defined as the composition of the left finitely supported function of $N$ and $x_{3}$ and the linear equivalence of $\operatorname{lid}$ applied to $R$ and $N$.

TensorProduct.finsuppScalarRightdefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the right finitely supported function scalar of M and x6 (from the name)

English

Let $R$, $S$, $M$ and $x_{6}$ be sets. Then the right finitely supported function scalar of $M$ and $x_{6}$ is a linear equivalence of the set of tensor products of $M$ and $\FinsuppMACRoQ {x_{6}}{R}$ and $\FinsuppMACRoQ {x_{6}}{M}$ defined as the composition of the right finitely supported function of $R$ and $x_{6}$ and the linear equivalence of $\operatorname{rid}$ applied to $R$, $S$ and $M$.

finsuppTensorFinsuppdefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the tensor product of R (from the docstring)

English

Let $R$, $S$, $M$, $N$, $x$ and $x_{1}$ be sets. Then the tensor product of $R$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{1}}{N}$ and the set of finitely supported functions from $\mathrm{Prod}$ applied to $x$ and $x_{1}$ to the set of tensor products of $M$ and $N$ defined as the composition of the congruence of the finitely supported function equivalence direct sum of $M$ and $x$ and the finitely supported function equivalence direct sum of $N$ and $x_{1}$ and the composition of the direct sum of the function that maps $x_{10}$ to $M$ and the function that maps $x_{11}$ to $N$ and the inverse of the finitely supported function equivalence direct sum of the set of tensor products of $M$ and $N$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

finsuppTensorFinsupp'defMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

the finitely supported function tensor finitely supported function of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the finitely supported function tensor finitely supported function of $x$ and $x_{1}$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x}{R}$ and $\FinsuppMACRoQ {x_{1}}{R}$ and $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{R}$ defined as $\mathrm{finsuppTensorFinsuppLid}$ applied to $R$, $R$, $x$ and $x_{1}$.

finsuppTensorFinsuppLiddefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

no wording

English

Let $R$, $N$, $x$ and $x_{1}$ be sets. Then $\mathrm{finsuppTensorFinsuppLid}$ applied to $R$, $N$, $x$ and $x_{1}$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x}{R}$ and $\FinsuppMACRoQ {x_{1}}{N}$ and $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{N}$ defined as 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{lid}$ applied to $R$ and $N$.

finsuppTensorFinsuppRiddefMathlib.LinearAlgebra.DirectSum.Finsupp, function or constant

Wording

no wording

English

Let $R$, $M$, $x$ and $x_{1}$ be sets. Then $\mathrm{finsuppTensorFinsuppRid}$ applied to $R$, $M$, $x$ and $x_{1}$ is a linear equivalence of the set of tensor products of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{1}}{R}$ and $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$ defined as 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$ and $M$.

Mathlib.LinearAlgebra.DirectSum.TensorProduct

TensorProduct.directSumdefMathlib.LinearAlgebra.DirectSum.TensorProduct, function or constant

Wording

the direct sum of x7 and x8 (from the name)

English

Let $R$ and $S$ be sets. Let $x_{7}$ be a function from elements of $x_{3}$ to sets. Let $x_{8}$ be a function from elements of $x_{4}$ to sets. Then the direct sum of $x_{7}$ and $x_{8}$ is a linear equivalence of the set of tensor products of the set of direct sums of $x_{3}$ and the function that maps $x_{14}$ to $x_{7}$ applied to $x_{14}$ and the set of direct sums of $x_{4}$ and the function that maps $x_{15}$ to $x_{8}$ applied to $x_{15}$ and the set of direct sums of $\mathrm{Prod}$ applied to $x_{3}$ and $x_{4}$ and the function that maps $i$ to the set of tensor products of $x_{7}$ applied to $\ProdfstMACRoZ {i}$ and $x_{8}$ applied to $\ProdsndMACRoAA {i}$.

TensorProduct.directSumLeftdefMathlib.LinearAlgebra.DirectSum.TensorProduct, function or constant

Wording

the left direct sum of x5 (from the name)

English

Let $R$, $S$ and $x_{6}$ be sets. Let $x_{5}$ be a function from elements of $x_{3}$ to sets. Then the left direct sum of $x_{5}$ is a linear equivalence of the set of tensor products of the set of direct sums of $x_{3}$ and the function that maps $x_{12}$ to $x_{5}$ applied to $x_{12}$ and $x_{6}$ and the set of direct sums of $x_{3}$ and the function that maps $i$ to the set of tensor products of $x_{5}$ applied to $i$ and $x_{6}$ defined as the composition of the composition of the congruence of $1$ and the inverse of $\operatorname{lid}$ applied to $R$, $x_{6}$ and $\mathrm{PUnit}$ and the direct sum of $x_{5}$ and the function that maps $x_{12}$ to $x_{6}$ and the left linear equivalence congruence of $S$ and $\operatorname{prodUnique}$ applied to $x_{3}$ and $\mathrm{Unit}$.

TensorProduct.directSumRightdefMathlib.LinearAlgebra.DirectSum.TensorProduct, function or constant

Wording

the right direct sum of x6 (from the name)

English

Let $R$, $S$ and $x_{5}$ be sets. Let $x_{6}$ be a function from elements of $x_{3}$ to sets. Then the right direct sum of $x_{6}$ is a linear equivalence of the set of tensor products of $x_{5}$ and the set of direct sums of $x_{3}$ and the function that maps $i$ to $x_{6}$ applied to $i$ and the set of direct sums of $x_{3}$ and the function that maps $i_{1}$ to the set of tensor products of $x_{5}$ and $x_{6}$ applied to $i_{1}$ defined as the composition of the composition of the congruence of the inverse of $\operatorname{lid}$ applied to $S$, $x_{5}$ and $\mathrm{PUnit}$ and $1$ and the direct sum of the function that maps $x_{12}$ to $x_{5}$ and $x_{6}$ and the left linear equivalence congruence of $S$ and the unique product of $x_{3}$ and $\mathrm{Unit}$.

Mathlib.LinearAlgebra.Dual.BaseChange

IsBaseChange.toDualdefMathlib.LinearAlgebra.Dual.BaseChange, function or constant

Wording

the base change of ibc (from the docstring)

English

Assume that $j$ is a base change. Then the base change of $\mathrm{ibc}$ is a linear map of the set of duals of $R$ and $V$ and the set of duals of $A$ and $W$ defined as the linear map left right homomorphism of $\mathrm{ibc}$ and the linear map of $R$ and $A$.

IsBaseChange.toDualBaseChangedefMathlib.LinearAlgebra.Dual.BaseChange, function or constant

Wording

the dual base change of ibc (from the name)

English

Assume that $j$ is a base change. Then the dual base change of $\mathrm{ibc}$ is a linear equivalence of the set of tensor products of $A$ and the set of duals of $R$ and $V$ and the set of duals of $A$ and $W$.

Module.Dual.baseChangedefMathlib.LinearAlgebra.Dual.BaseChange, function or constant

Wording

the base change of A (from the name)

English

Let $A$ be a set. Then the base change of $A$ is a linear map of the set of duals of $R$ and $V$ and the set of duals of $A$ and the set of tensor products of $A$ and $V$ defined as the composition of the right composition of $R$ and $\operatorname{toLinearMap}$ applied to $\operatorname{rid}$ applied to $R$, $A$ and $A$ and the base change homomorphism of $V$ and $R$.

Module.Dual.congrdefMathlib.LinearAlgebra.Dual.BaseChange, function or constant

Wording

the congruence of e (from the name)

English

Let $e$ be a linear equivalence of $V$ and $W$. Then the congruence of $e$ is a linear equivalence of the set of duals of $R$ and $V$ and the set of duals of $R$ and $W$ defined as the left congruence of $e$.