Definitions: Mathlib.LinearAlgebra, part 2 of 5

Module.Basis.dualBasisdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

the dual basis of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the dual basis of $b$ is a basis of $R$ and the set of duals of $R$ and $M$ defined as the map of $b$ and the dual equivalence of $b$.

Module.Basis.toDualdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

the dual of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the dual of $b$ is a linear map of $M$ and the set of duals of $R$ and $M$ defined as $\operatorname{constr}$ applied to $b$, $\Natural$ and the function that maps $v_{1}$ to $\operatorname{constr}$ applied to $b$, $\Natural$ and the function that maps $w$ to $\iteMACRoG {(\EqtMACRoH {w}{v_{1}})}{1}{0}$.

Module.Basis.toDualEquivdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

the dual equivalence of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the dual equivalence of $b$ is a linear equivalence of $M$ and the set of duals of $R$ and $M$.

Module.Basis.toDualFlipdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

the dual flip of b and m (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $m$ be an element of $M$. Then the dual flip of $b$ and $m$ is a linear map of $M$ and $R$ defined as $\operatorname{flip}$ applied to the dual of $b$ and $m$.

Module.DualBasesstructureMathlib.LinearAlgebra.Dual.Basis, predicate

Wording

no wording

English

Let $e$ be a function from elements of $x$ to elements of $M$. Let $x_{4}$ be a function from elements of $x$ to duals of $R$ and $M$. Then we can say that $\operatorname{DualBases}$ holds for $e$ and $x_{4}$.

Module.DualBases.basisdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

the basis of h (from the name)

English

Assume that $\operatorname{DualBases}$ holds for $e$ and $x_{4}$. Then the basis of $h$ is a basis of $R$ and $M$.

Module.DualBases.coeffsdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

no wording

English

Assume that $\operatorname{DualBases}$ holds for $e$ and $x_{4}$. Let $m$ be an element of $M$. Then $\operatorname{coeffs}$ applied to $h$ and $m$ is an element of $\FinsuppMACRoQ {x}{R}$.

Module.DualBases.lcdefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

no wording

English

Let $e$ be a function from elements of $x_{3}$ to elements of $M$. Let $l$ be an element of $\FinsuppMACRoQ {x_{3}}{R}$. Then $\operatorname{lc}$ applied to $e$ and $l$ is an element of $M$ defined as the sum of $l$ and the function that maps $i$ and $a$ to $\HSMulhSMulMACRoAL {a}{e (i)}$.

evalUseFiniteInstancedefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

no wording

English

generation took over the time limit

tacticUse_finite_instancedefMathlib.LinearAlgebra.Dual.Basis, function or constant

Wording

no wording

English

generation took over the time limit

Mathlib.LinearAlgebra.Dual.Defs

LinearEquiv.dualMapdefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the dual map of f (from the name)

English

Let $f$ be a linear equivalence of $x$ and $x_{1}$. Then the dual map of $f$ is a linear equivalence of the set of duals of $R$ and $x_{1}$ and the set of duals of $R$ and $x$.

LinearMap.dualMapdefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the dual map of f (from the name)

English

Let $f$ be a linear map of $x$ and $x_{1}$. Then the dual map of $f$ is a linear map of the set of duals of $R$ and $x_{1}$ and the set of duals of $R$ and $x$ defined as $\operatorname{transpose}$ applied to $f$.

Module.DualdefMathlib.LinearAlgebra.Dual.Defs, type

Wording

dual of R and M (from the name)

English

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

Module.Dual.evaldefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the evaluation of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the evaluation of $R$ and $M$ is a linear map of $M$ and the set of duals of $R$ and the set of duals of $R$ and $M$ defined as the flip of the identity.

Module.Dual.transposedefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the transpose (from the name)

English

The transpose is a linear map of the set of linear maps of $M$ and $\mathrm{M'}$ and the set of linear maps of the set of duals of $R$ and $\mathrm{M'}$ and the set of duals of $R$ and $M$ defined as the flip of $\operatorname{llcomp}$ applied to $R$, $M$, $\mathrm{M'}$ and $R$.

Module.IsReflexiveclassMathlib.LinearAlgebra.Dual.Defs, predicate

Wording

no wording

English

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

Module.evalEquivdefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the evaluation equivalence of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the evaluation equivalence of $R$ and $M$ is a linear equivalence of $M$ and the set of duals of $R$ and the set of duals of $R$ and $M$ defined as the linear equivalence of the evaluation of $R$ and $M$ and $\mathrm{Module\_\_bijective\_dual\_eval}$ applied to $R$ and $M$.

Module.mapEvalEquivdefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the map evaluation equivalence of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the map evaluation equivalence of $R$ and $M$ is an order isomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $R$ and the set of duals of $R$ and the set of duals of $R$ and $M$ defined as the order isomorphism map preimage of the evaluation equivalence of $R$ and $M$.

Submodule.dualAnnihilatordefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

the dual annihilator of W (from the name)

English

Let $W$ be a submodule of $R$ and $M$. Then the dual annihilator of $W$ is a submodule of $R$ and the set of duals of $R$ and $M$ defined as the kernel of $\operatorname{dualRestrict}$ applied to $W$.

Submodule.dualCoannihilatordefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

no wording

English

Let $x_{3}$ be a submodule of $R$ and the set of duals of $R$ and $M$. Then $\operatorname{dualCoannihilator}$ applied to $x_{3}$ is a submodule of $R$ and $M$ defined as the preimage of the evaluation of $R$ and $M$ and the dual annihilator of $x_{3}$.

Submodule.dualRestrictdefMathlib.LinearAlgebra.Dual.Defs, function or constant

Wording

no wording

English

Let $W$ be a submodule of $R$ and $M$. Then $\operatorname{dualRestrict}$ applied to $W$ is a linear map of the set of duals of $R$ and $M$ and the set of duals of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ defined as $\operatorname{domRestrict'}$ applied to $W$.

Mathlib.LinearAlgebra.Dual.Lemmas

Module.dualProdDualEquivDualdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the dual product dual equivalence dual of M and #3 (from the name)

English

Let $R$, $M$ and $\mathrm{M'}$ be sets. Then the dual product dual equivalence dual of $M$ and $\mathrm{M'}$ is a linear equivalence of $\mathrm{Prod}$ applied to the set of duals of $R$ and $M$ and the set of duals of $R$ and $\mathrm{M'}$ and the set of duals of $R$ and $\mathrm{Prod}$ applied to $M$ and $\mathrm{M'}$ defined as the coproduct equivalence of $R$.

Submodule.dualCopairingdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

Let $W$ be a submodule of $R$ and $M$. Then $\operatorname{dualCopairing}$ applied to $W$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{dualAnnihilator} (W)}{x_{3}})}$ and the set of linear maps of the set of quotients of $M$ and $W$ and $R$.

Submodule.dualPairingdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the dual pairing of W (from the name)

English

Let $W$ be a submodule of $R$ and $M$. Then the dual pairing of $W$ is a linear map of the set of quotients of the set of duals of $R$ and $M$ and the dual annihilator of $W$ and the set of linear maps of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ and $R$.

Submodule.dualQuotEquivDualAnnihilatordefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the dual quotient equivalence dual annihilator of W (from the name)

English

Let $W$ be a submodule of $R$ and $M$. Then the dual quotient equivalence dual annihilator of $W$ is a linear equivalence of the set of duals of $R$ and the set of quotients of $M$ and $W$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{dualAnnihilator} (W)}{x_{3}})}$.

Submodule.quotDualCoannihilatorToDualdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

Let $W$ be a submodule of $R$ and the set of duals of $R$ and $M$. Then $\operatorname{quotDualCoannihilatorToDual}$ applied to $W$ is a linear map of the set of quotients of $M$ and $\operatorname{dualCoannihilator}$ applied to $W$ and the set of duals of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$.

Subspace.dualAnnihilatorGcidefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

Let $K$ and $V$ be sets. Then $\operatorname{dualAnnihilatorGci}$ applied to $K$ and $V$ is a Galois coinsertion of $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to the dual and $\operatorname{dualAnnihilator}$ and $\operatorname{comp}$ applied to $\operatorname{dualCoannihilator}$ and $\operatorname{coe}$ applied to the order dual.

Subspace.dualEquivDualdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the natural isomorphism from the dual of W (from the docstring)

English

Let $W$ be a subspace of $K$ and $V$. Then the natural isomorphism from the dual of $W$ is a linear equivalence of the set of duals of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{range} (\operatorname{dualLift} (W))}{x_{4}})}$ defined as the linear equivalence of the dual lift of $W$ and $\mathrm{Subspace\_\_dualLift\_injective}$.

Subspace.dualLiftdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the dual lift of W (from the name)

English

Let $W$ be a subspace of $K$ and $V$. Then the dual lift of $W$ is a linear map of the set of duals of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ and the set of duals of $K$ and $V$ defined as the dual map of the left inverse of the subtype of $W$.

Subspace.dualQuotDistribdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

Let $W$ be a subspace of $K$ and $x$. Then $\operatorname{dualQuotDistrib}$ applied to $W$ is a linear equivalence of the set of duals of $K$ and the set of quotients of $x$ and $W$ and the set of quotients of the set of duals of $K$ and $x$ and the range of the dual lift of $W$ defined as the composition of the dual quotient equivalence dual annihilator of $W$ and the inverse of the quotient by the dual of $W$.

Subspace.orderIsoFiniteCodimDimdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

$\operatorname{orderIsoFiniteCodimDim}$ is an order isomorphism of $\SubtypeSet {W}{\mathrm{FiniteDimensional} (K , \operatorname{Quotient} (V , W))}$ and the set of order duals of $\SubtypeSet {W_{1}}{\mathrm{FiniteDimensional} (K , \SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W_{1}}{x_{3}})})}$.

Subspace.orderIsoFiniteDimensionaldefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

$\operatorname{orderIsoFiniteDimensional}$ is an order isomorphism of the set of subspaces of $K$ and $V$ and the set of order duals of the set of subspaces of $K$ and the set of duals of $K$ and $V$.

Subspace.quotAnnihilatorEquivdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the quotient annihilator equivalence of W (from the name)

English

Let $W$ be a subspace of $K$ and $V$. Then the quotient annihilator equivalence of $W$ is a linear equivalence of the set of quotients of the set of duals of $K$ and $V$ and the dual annihilator of $W$ and the set of duals of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$.

Subspace.quotDualEquivAnnihilatordefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the quotient by the dual of W (from the docstring)

English

Let $W$ be a subspace of $K$ and $V$. Then the quotient by the dual of $W$ is a linear equivalence of the set of quotients of the set of duals of $K$ and $V$ and the range of the dual lift of $W$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{dualAnnihilator} (W)}{x_{3}})}$ defined as the quotient equivalence of the composition of the quotient annihilator equivalence of $W$ and the natural isomorphism from the dual of $W$.

Subspace.quotEquivAnnihilatordefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

the quotient by a subspace of W (from the docstring)

English

Let $W$ be a subspace of $K$ and $V$. Then the quotient by a subspace of $W$ is a linear equivalence of the set of quotients of $V$ and $W$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{dualAnnihilator} (W)}{x_{3}})}$ defined as the composition of the quotient equivalence of the composition of the dual equivalence of the basis of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {W}{x_{3}})}$ and the natural isomorphism from the dual of $W$ and the dual equivalence of the basis of $K$ and $V$ and the quotient by the dual of $W$.

TensorProduct.AlgebraTensorModule.dualDistribdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

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

TensorProduct.dualDistribdefMathlib.LinearAlgebra.Dual.Lemmas, function or constant

Wording

no wording

English

Let $R$, $M$ and $N$ be sets. Then $\operatorname{dualDistrib}$ applied to $R$, $M$ and $N$ is a linear map 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 right composition of $R$ and $\operatorname{toLinearMap}$ applied to $\operatorname{lid}$ applied to $R$ and $R$ and the homomorphism tensor homomorphism map of the identity ring homomorphism of $R$.

Mathlib.LinearAlgebra.Eigenspace.Basic

Module.End.EigenvaluesdefMathlib.LinearAlgebra.Eigenspace.Basic, type

Wording

eigenvalue of f (from the name)

English

Let $f$ be an end of $R$ and $M$. Then an eigenvalue of $f$ is an element of the function that maps $f$ to the set of uniform eigenvalues of $f$ and $1$.

Module.End.Eigenvalues.valdefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the value of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an eigenvalue of $f$. Then the value of $f$ and $x_{3}$ is an element of $R$ defined as the value of $1$ and $x_{3}$.

Module.End.HasEigenvaluedefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $a$ be an element of $R$. Then $\operatorname{HasEigenvalue}$ holds for $f$ and $a$, if $\operatorname{HasUnifEigenvalue}$ holds for $f$, $a$ and $1$.

Module.End.HasEigenvectordefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $x_{4}$ be an element of $M$. Then $\operatorname{HasEigenvector}$ holds for $f$, $x_{3}$ and $x_{4}$, if $\operatorname{HasUnifEigenvector}$ holds for $f$, $x_{3}$, $1$ and $x_{4}$.

Module.End.HasGenEigenvaluedefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $k$ be a natural number. Then $\operatorname{HasGenEigenvalue}$ holds for $f$, $x_{3}$ and $k$, if $\operatorname{HasUnifEigenvalue}$ holds for $f$, $x_{3}$ and $k$.

Module.End.HasGenEigenvectordefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $k$ be a natural number. Let $x_{4}$ be an element of $M$. Then $\operatorname{HasGenEigenvector}$ holds for $f$, $x_{3}$, $k$ and $x_{4}$, if $\operatorname{HasUnifEigenvector}$ holds for $f$, $x_{3}$, $k$ and $x_{4}$.

Module.End.HasUnifEigenvaluedefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $k$ be a natural number. Then $\operatorname{HasUnifEigenvalue}$ holds for $f$, $x_{3}$ and $k$, if $\operatorname{genEigenspace}$ applied to $f$, $x_{3}$ and $k$ is distinct from the bottom.

Module.End.HasUnifEigenvectordefMathlib.LinearAlgebra.Eigenspace.Basic, predicate

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $k$ be a natural number. Let $x_{4}$ be an element of $M$. Then $\operatorname{HasUnifEigenvector}$ holds for $f$, $x_{3}$, $k$ and $x_{4}$, if $\MembershipmemMACRoT {\operatorname{genEigenspace} (f , x_{3} , k)}{x_{4}}$ and $x_{4} \neq 0$.

Module.End.UnifEigenvaluesdefMathlib.LinearAlgebra.Eigenspace.Basic, type

Wording

uniform eigenvalue of f and k (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $k$ be a natural number. Then a uniform eigenvalue of $f$ and $k$ is an element of the function that maps $f$ and $k$ to $\SubtypeSet {x_{3}}{\operatorname{HasUnifEigenvalue} (f , x_{3} , k)}$.

Module.End.UnifEigenvalues.valdefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the value of k and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $k$ be a natural number. Let $x_{3}$ be a uniform eigenvalue of $f$ and $k$. Then the value of $k$ and $x_{3}$ is an element of $R$ defined as $\operatorname{HasUnifEigenvalue}$ applied to $f$, $x_{3}$ and $k$.

Module.End.eigenspacedefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the eigenspace of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Then the eigenspace of $f$ and $x_{3}$ is a submodule of $R$ and $M$ defined as $\operatorname{genEigenspace}$ applied to $f$, $x_{3}$ and $1$.

Module.End.genEigenrangedefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Let $k$ be a natural number. Then $\operatorname{genEigenrange}$ applied to $f$, $x_{3}$ and $k$ is a submodule of $R$ and $M$ defined as the infimum of the function that maps $l$ to the infimum of the function that maps $h$ to the range of $(f - \HSMulhSMulMACRoAL {x_{3}}{1})^ {l}$.

Module.End.genEigenspacedefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the generator eigenspace of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Then the generator eigenspace of $f$ and $x_{3}$ is an order homomorphism of the set of natural numbers and the set of submodules of $R$ and $M$.

Module.End.maxGenEigenspacedefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the maximum generator eigenspace of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Then the maximum generator eigenspace of $f$ and $x_{3}$ is a submodule of $R$ and $M$ defined as $\operatorname{genEigenspace}$ applied to $f$, $x_{3}$ and the top.

Module.End.maxGenEigenspaceIndexdefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the maximum generator eigenspace index of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Then the maximum generator eigenspace index of $f$ and $x_{3}$ is a natural number defined as the maximum uniform eigenspace index of $f$ and $x_{3}$.

Module.End.maxUnifEigenspaceIndexdefMathlib.LinearAlgebra.Eigenspace.Basic, function or constant

Wording

the maximum uniform eigenspace index of f and x3 (from the name)

English

Let $f$ be an end of $R$ and $M$. Let $x_{3}$ be an element of $R$. Then the maximum uniform eigenspace index of $f$ and $x_{3}$ is a natural number defined as the monotonic sequence limit index of the composition of the generator eigenspace of $f$ and $x_{3}$ and the order homomorphism of the coercion.

Mathlib.LinearAlgebra.ExteriorAlgebra.BaseChange

ExteriorAlgebra.baseChangeEquivdefMathlib.LinearAlgebra.ExteriorAlgebra.BaseChange, function or constant

Wording

the base change equivalence of M and S (from the name)

English

Let $R$, $M$ and $S$ be sets. Then the base change equivalence of $M$ and $S$ is an algebra isomorphism of the set of tensor products of $S$ and the set of exterior algebras of $R$ and $M$ and the set of exterior algebras of $S$ and the set of tensor products of $S$ and $M$.

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

ExteriorAlgebradefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, type

Wording

exterior algebra of R and M (from the name)

English

Let $R$ and $M$ be sets. Then an exterior algebra of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of Clifford algebras of $0$.

ExteriorAlgebra.algebraMapInvdefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the algebra map inverse (from the name)

English

The algebra map inverse is an algebra homomorphism of the set of exterior algebras of $R$ and $M$ and $R$ defined as $\operatorname{lift}$ applied to $R$ and $0$.

ExteriorAlgebra.exteriorPowerdefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the exterior power of n (from the name)

English

Let $R$ and $M$ be sets. Let $n$ be a natural number. Then the exterior power of $n$ is a submodule of $R$ and the set of exterior algebras of $R$ and $M$ defined as the exponentiation of the range of the inclusion of $R$ to $n$.

ExteriorAlgebra.invertibleAlgebraMapEquivdefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the invertible algebra map equivalence of M and r (from the name)

English

Let $M$ be a set. Let $r$ be an element of $R$. Then the invertible algebra map equivalence of $M$ and $r$ is an equivalence from the proposition that $\operatorname{algebraMap}$ applied to $R$, the set of exterior algebras of $R$ and $M$ and $r$ is invertible to the proposition that $r$ is invertible defined as the invertible equivalence of the algebra map inverse and $r$.

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

Wording

the lift of R (from the name)

English

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

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

Wording

the map of f (from the name)

English

Let $f$ be a linear map of $M$ and $N$. Then the map of $f$ is an algebra homomorphism of the set of exterior algebras of $R$ and $M$ and the set of exterior algebras of $R$ and $N$.

ExteriorAlgebra.toTrivSqZeroExtdefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the trivial square zero extension (from the name)

English

The trivial square zero extension is an algebra homomorphism of the set of exterior algebras of $R$ and $M$ and the set of trivial square zero extensions of $R$ and $M$ defined as $\operatorname{lift}$ applied to $R$ and the right injection homomorphism of $R$ and $M$.

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

Wording

the inclusion of R (from the name)

English

Let $R$ be a set. Then the inclusion of $R$ is a linear map of $M$ and the set of exterior algebras of $R$ and $M$ defined as the inclusion of $0$.

ExteriorAlgebra.ιInvdefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the inclusion inverse (from the name)

English

The inclusion inverse is a linear map of the set of exterior algebras of $R$ and $M$ and $M$ defined as the composition of the second component homomorphism of $R$ and $M$ and the linear map of the trivial square zero extension.

ExteriorAlgebra.ιMultidefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then $\mathrm{ExteriorAlgebra\_\_\_u3b9\_Multi}$ applied to $R$ and $n$ is an alternating map of the set of exterior algebras of $R$ and $M$ and $\mathrm{Fin}$ applied to $n$.

ExteriorAlgebra.ιMulti_familydefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the inclusion multi family of v and s (from the name)

English

Let $R$ be a set. Let $n$ be a natural number. Let $v$ be a function from elements of $I$ to elements of $M$. Let $s$ be an element of the powerset cardinality of $I$ and $n$. Then the inclusion multi family of $v$ and $s$ is an exterior algebra of $R$ and $M$ defined as $\mathrm{ExteriorAlgebra\_\_\_u3b9\_Multi\_\_app}$ applied to $R$, $n$ and $\operatorname{comp}$ applied to $v$ and $\operatorname{coe}$ applied to $\operatorname{symm}$ applied to the powerset cardinality and $s$.

TensorAlgebra.toExteriordefMathlib.LinearAlgebra.ExteriorAlgebra.Basic, function or constant

Wording

the exterior (from the name)

English

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

Mathlib.LinearAlgebra.ExteriorAlgebra.Basis

Module.Basis.ExteriorAlgebradefMathlib.LinearAlgebra.ExteriorAlgebra.Basis, function or constant

Wording

the exterior algebra of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the exterior algebra of $b$ is a basis of $R$ and the set of exterior algebras of $R$ and $M$.

Mathlib.LinearAlgebra.ExteriorAlgebra.Grading

ExteriorAlgebra.GradedAlgebra.liftιdefMathlib.LinearAlgebra.ExteriorAlgebra.Grading, function or constant

Wording

the lift inclusion of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the lift inclusion of $R$ and $M$ is an algebra homomorphism of the set of exterior algebras of $R$ and $M$ and the set of direct sums of $\Natural$ and the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (i)}{x_{3}})}$ defined as $\operatorname{lift}$ applied to $R$ and the inclusion of $R$ and $M$.

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

Wording

the inclusion of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the inclusion of $R$ and $M$ is a linear map of $M$ and the set of direct sums of $\Natural$ and the function that maps $i$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (i)}{x_{3}})}$.

Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

ExteriorAlgebra.liftAlternatingdefMathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating, function or constant

Wording

no wording

English

$\operatorname{liftAlternating}$ is a linear map of the set of functions from natural numbers $i$ to alternating maps of $N$ and $\mathrm{Fin}$ applied to $i$ and the set of linear maps of the set of exterior algebras of $R$ and $M$ and $N$.

ExteriorAlgebra.liftAlternatingEquivdefMathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating, function or constant

Wording

the equivalence (from the docstring)

English

The equivalence is a linear equivalence of the set of functions from natural numbers $i$ to alternating maps of $N$ and $\mathrm{Fin}$ applied to $i$ and the set of linear maps of the set of exterior algebras of $R$ and $M$ and $N$.

Mathlib.LinearAlgebra.ExteriorAlgebra.Product

ExteriorAlgebra.prodEquivTensordefMathlib.LinearAlgebra.ExteriorAlgebra.Product, function or constant

Wording

the product equivalence tensor of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the product equivalence tensor of $M$ and $N$ is an algebra isomorphism of the set of exterior algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of graded tensor products of the function that maps $i$ to the exterior power of $i$ and the function that maps $i_{1}$ to the exterior power of $i_{1}$ defined as the algebra isomorphism of $\operatorname{prodEquivTensorForward}$ applied to $R$, $M$ and $N$ and the product equivalence tensor inverse of $M$ and $N$.

ExteriorAlgebra.prodEquivTensorForwarddefMathlib.LinearAlgebra.ExteriorAlgebra.Product, function or constant

Wording

no wording

English

Let $R$, $M$ and $N$ be sets. Then $\operatorname{prodEquivTensorForward}$ applied to $R$, $M$ and $N$ is an algebra homomorphism of the set of exterior algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of graded tensor products of the function that maps $i$ to the exterior power of $i$ and the function that maps $i_{1}$ to the exterior power of $i_{1}$.

ExteriorAlgebra.prodEquivTensorInversedefMathlib.LinearAlgebra.ExteriorAlgebra.Product, function or constant

Wording

the product equivalence tensor inverse of M and N (from the name)

English

Let $R$, $M$ and $N$ be sets. Then the product equivalence tensor inverse of $M$ and $N$ is an algebra homomorphism of the set of graded tensor products of the function that maps $i$ to the exterior power of $i$ and the function that maps $i_{1}$ to the exterior power of $i_{1}$ and the set of exterior algebras of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$ defined as the lift of the map of the left injection of $M$ and $N$ and the map of the right injection of $M$ and $N$.

Mathlib.LinearAlgebra.ExteriorPower.Basic

exteriorPower.alternatingMapLinearEquivdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the alternating map linear equivalence (from the name)

English

The alternating map linear equivalence is a linear equivalence of the set of alternating maps of $N$ and $\mathrm{Fin}$ applied to $n$ and the set of linear maps of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{5}})}$ and $N$.

exteriorPower.mapdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the map of n and f (from the name)

English

Let $n$ be an element of $\Natural$. Let $f$ be a linear map of $M$ and $N$. Then the map of $n$ and $f$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{6}})}$ defined as $\operatorname{alternatingMapLinearEquiv}$ applied to the composition linear map of $\mathrm{exteriorPower\_\_\_u3b9\_Multi}$ applied to $R$ and $n$ and $f$.

exteriorPower.oneEquivdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the linear equivalence of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the linear equivalence of $R$ and $M$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (1)}{x_{3}})}$ and $M$.

exteriorPower.presentationdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the presentation of n (from the name)

English

Let $R$ and $M$ be sets. Let $n$ be an element of $\Natural$. Then the presentation of $n$ is a presentation of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$.

exteriorPower.presentation.RelsinductiveMathlib.LinearAlgebra.ExteriorPower.Basic, type

Wording

no wording

English

Let $R$, $x$ and $M$ be sets. Then the elements of $\operatorname{Rels}$ applied to $R$, $x$ and $M$ are a basic type.

exteriorPower.presentation.Rels.addconstructorMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the sum of x1 and y (from the name)

English

Let $m$ be a function from elements of $x$ to elements of $M$. Let $i$ be an element of $x$. Let $x_{1}$ and $y$ be elements of $M$. Then the sum of $x_{1}$ and $y$ is an element of $\operatorname{Rels}$ applied to $R$, $x$ and $M$.

exteriorPower.presentation.Rels.altconstructorMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

no wording

English

Let $m$ be a function from elements of $x$ to elements of $M$. Let $i$ and $j$ be elements of $x$ such that $\EqtMACRoH {m (i)}{m (j)}$ and $i \neq j$. Then $\operatorname{alt}$ applied to $m$, $i$, $j$, $\mathrm{hm}$ and $\mathrm{hij}$ is an element of $\operatorname{Rels}$ applied to $R$, $x$ and $M$.

exteriorPower.presentation.Rels.ctorElimTypedefMathlib.LinearAlgebra.ExteriorPower.Basic, type

Wording

no wording

English

Let $\mathrm{ctorIdx}$ be a natural number. Then an element of $\operatorname{ctorElimType}$ applied to $\mathrm{ctorIdx}$ is an element of the function that maps $\mathrm{ctorIdx}$ to $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $0$, $\mathrm{PULift}$ applied to the set of functions from functions $m$ from elements of $x$ to elements of $M$ and elements $i$ of $x$ and elements $x_{1}$ of $M$ and elements $y$ of $M$ to elements of $\mathrm{motive}$ applied to the sum of $x_{1}$ and $y$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from functions $m_{1}$ from elements of $x$ to elements of $M$ and elements $i_{1}$ of $x$ and elements $r$ of $R$ and elements $x_{3}$ of $M$ to elements of $\mathrm{motive}$ applied to the scalar multiple of $r$ and $x_{3}$ and $\mathrm{PULift}$ applied to the set of functions from functions $m_{2}$ from elements of $x$ to elements of $M$ and elements $i_{2}$ of $x$ and elements $j$ of $x$ and elements $\mathrm{hm}$ of $\mathrm{Proof}$ applied to $\EqtMACRoH {m_{2} (i_{2})}{m_{2} (j)}$ and elements $\mathrm{hij}$ of $\mathrm{Proof}$ applied to $\mathrm{Neq} (i_{2} , j)$ to elements of $\mathrm{motive}$ applied to $\operatorname{alt}$ applied to $m_{2}$, $i_{2}$, $j$, $\mathrm{hm}$ and $\mathrm{hij}$.

exteriorPower.presentation.Rels.smulconstructorMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the scalar multiple of r and x1 (from the name)

English

Let $m$ be a function from elements of $x$ to elements of $M$. Let $i$ be an element of $x$. Let $r$ be an element of $R$. Let $x_{1}$ be an element of $M$. Then the scalar multiple of $r$ and $x_{1}$ is an element of $\operatorname{Rels}$ applied to $R$, $x$ and $M$.

exteriorPower.presentation.isPresentationCoredefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Let $n$ be a natural number. Then $\operatorname{isPresentationCore}$ applied to $R$, $n$ and $M$ is an element of $\operatorname{IsPresentationCore}$ applied to $\operatorname{symm}$ applied to the relation solution equivalence and $\mathrm{exteriorPower\_\_\_u3b9\_Multi}$ applied to $R$ and $n$.

exteriorPower.presentation.relationsdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the relation of x1 and M (from the name)

English

Let $R$, $x_{1}$ and $M$ be sets. Then the relation of $x_{1}$ and $M$ is a relation of $R$.

exteriorPower.presentation.relationsSolutionEquivdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the relation solution equivalence (from the name)

English

The relation solution equivalence is an equivalence from the set of solutions of the relation of $x_{3}$ and $M$ and $N$ to the set of alternating maps of $N$ and $x_{3}$.

exteriorPower.zeroEquivdefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the linear equivalence of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the linear equivalence of $R$ and $M$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (0)}{x_{3}})}$ and $R$.

exteriorPower.ιMultidefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $n$ be an element of $\Natural$. Then $\mathrm{exteriorPower\_\_\_u3b9\_Multi}$ applied to $R$ and $n$ is an alternating map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$ and $\mathrm{Fin}$ applied to $n$.

exteriorPower.ιMulti_familydefMathlib.LinearAlgebra.ExteriorPower.Basic, function or constant

Wording

the inclusion multi family of v and s (from the name)

English

Let $R$ be a set. Let $n$ be an element of $\Natural$. Let $v$ be a function from elements of $I$ to elements of $M$. Let $s$ be an element of the powerset cardinality of $I$ and $n$. Then the inclusion multi family of $v$ and $s$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{4}})}$ defined as $\mathrm{exteriorPower\_\_\_u3b9\_Multi\_\_app}$ applied to $R$, $n$ and $\operatorname{comp}$ applied to $v$ and $\operatorname{coe}$ applied to $\operatorname{symm}$ applied to the powerset cardinality and $s$.

Mathlib.LinearAlgebra.ExteriorPower.Basis

Module.Basis.exteriorPowerdefMathlib.LinearAlgebra.ExteriorPower.Basis, function or constant

Wording

the exterior power of n and b (from the name)

English

Let $n$ be an element of $\Natural$. Let $b$ be a basis of $R$ and $M$. Then the exterior power of $n$ and $b$ is a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{4}})}$.

exteriorPower.ιMultiDualdefMathlib.LinearAlgebra.ExteriorPower.Basis, function or constant

Wording

the inclusion multi dual of b and s (from the name)

English

Let $R$ be a set. Let $n$ be an element of $\Natural$. Let $b$ be a basis of $R$ and $M$. Let $s$ be an element of the powerset cardinality of $I$ and $n$. Then the inclusion multi dual of $b$ and $s$ is a dual of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{4}})}$ defined as $\operatorname{pairingDual}$ applied to $R$, $M$, $n$ and the inclusion multi family of $\operatorname{coord}$ applied to $b$ and $s$.

Mathlib.LinearAlgebra.ExteriorPower.BilinForm

LinearMap.BilinForm.exteriorPowerdefMathlib.LinearAlgebra.ExteriorPower.BilinForm, function or constant

Wording

the exterior power of B and n (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $n$ be an element of $\Natural$. Then the exterior power of $B$ and $n$ is a bilinear form of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$ defined as the composition of the pairing dual of $n$ and the map of $n$ and $B$.

Mathlib.LinearAlgebra.ExteriorPower.HodgeStar

exteriorPower.hodgeStardefMathlib.LinearAlgebra.ExteriorPower.HodgeStar, function or constant

Wording

no wording

English

Let $B$ be a bilinear form of $R$ and $M$ such that $\operatorname{coe}$ applied to $B$ is bijective. Let $\mathrm{vol}$ be a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (\operatorname{finrank} (R , M))}{x_{5}})}$ and $R$. Assume that $k + l = \operatorname{finrank} (R , M)$. Then $\operatorname{hodgeStar}$ applied to $B$, $\mathrm{hB}$, $\mathrm{vol}$ and $\mathrm{hkl}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (k)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (l)}{x_{4}})}$ defined as the composition of $\operatorname{toPerfPair}$ applied to the wedge pairing of $\mathrm{vol}$ and $\mathrm{hkl}$ and the inverse of the linear equivalence of the exterior power of $B$ and $l$ and $\mathrm{LinearMap\_\_BilinForm\_\_bijective\_exteriorPower}$ applied to $B$, $l$ and $\mathrm{hB}$.

Mathlib.LinearAlgebra.ExteriorPower.Pairing

exteriorPower.alternatingMapToDualdefMathlib.LinearAlgebra.ExteriorPower.Pairing, function or constant

Wording

the alternating map to dual of n (from the name)

English

Let $R$ and $M$ be sets. Let $n$ be an element of $\Natural$. Then the alternating map to dual of $n$ is an alternating map of the set of duals of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$ and $\mathrm{Fin}$ applied to $n$.

exteriorPower.pairingDualdefMathlib.LinearAlgebra.ExteriorPower.Pairing, function or constant

Wording

the pairing dual of n (from the name)

English

Let $R$ and $M$ be sets. Let $n$ be an element of $\Natural$. Then the pairing dual of $n$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$ and the set of duals of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{4}})}$ defined as $\operatorname{alternatingMapLinearEquiv}$ applied to the alternating map to dual of $n$.

exteriorPower.toTensorPowerdefMathlib.LinearAlgebra.ExteriorPower.Pairing, function or constant

Wording

the tensor power of n (from the name)

English

Let $R$ and $M$ be sets. Let $n$ be an element of $\Natural$. Then the tensor power of $n$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (n)}{x_{3}})}$ and the set of tensor powers of $n$ and $M$ defined as $\operatorname{alternatingMapLinearEquiv}$ applied to $\operatorname{alternatization}$ applied to $\operatorname{tprod}$ applied to $R$.

Mathlib.LinearAlgebra.ExteriorPower.WedgePairing

Module.Basis.topVectordefMathlib.LinearAlgebra.ExteriorPower.WedgePairing, function or constant

Wording

the top vector of b (from the name)

English

Let $b$ be a basis of $R$ and $M$. Then the top vector of $b$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (\operatorname{finrank} (R , M))}{x_{6}})}$ defined as $\operatorname{exteriorPower}$ applied to the rank of $R$ and $M$, $b$ and $\FinsetunivMACRoAC$.

exteriorPower.wedgedefMathlib.LinearAlgebra.ExteriorPower.WedgePairing, function or constant

Wording

the wedge of k and l (from the name)

English

Let $R$ and $M$ be sets. Let $k$ and $l$ be elements of $\Natural$. Then the wedge of $k$ and $l$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (k)}{x_{3}})}$ and the set of linear maps of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (l)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (k + l)}{x_{5}})}$ defined as the multiplicative homomorphism of $R$ and the function that maps $d$ to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (d)}{x_{3}})}$.

exteriorPower.wedgePairingdefMathlib.LinearAlgebra.ExteriorPower.WedgePairing, function or constant

Wording

the wedge pairing of vol and hkl (from the name)

English

Let $\mathrm{vol}$ be a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (\operatorname{finrank} (R , M))}{x_{5}})}$ and $R$. Assume that $k + l = \operatorname{finrank} (R , M)$. Then the wedge pairing of $\mathrm{vol}$ and $\mathrm{hkl}$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (k)}{x_{3}})}$ and the set of linear maps of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{exteriorPower} (l)}{x_{4}})}$ and $R$.

Mathlib.LinearAlgebra.FiniteDimensional.Basic

FiniteDimensional.basisSingletondefMathlib.LinearAlgebra.FiniteDimensional.Basic, function or constant

Wording

the basis singleton of v (from the name)

English

Let $x_{3}$ be a set. Assume that the rank of $K$ and $V$ is equal to $1$. Let $v$ be an element of $V$ such that $v \neq 0$. Then the basis singleton of $v$ is a basis of $K$ and $V$.

LinearEquiv.ofInjectiveEndodefMathlib.LinearAlgebra.FiniteDimensional.Basic, function or constant

Wording

the linear equivalence corresponding to an injective endomorphism of f and h_inj (from the docstring)

English

Let $f$ be a linear map of $V$ and $V$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the linear equivalence corresponding to an injective endomorphism of $f$ and $\mathrm{h\_inj}$ is a linear equivalence of $V$ and $V$.

LinearEquiv.ofInjectiveOfFinrankEqdefMathlib.LinearAlgebra.FiniteDimensional.Basic, function or constant

Wording

the linear equivalence of f (from the name)

English

Let $f$ be a linear map of $V$ and $\mathrm{V'}$ such that $\operatorname{coe}$ applied to $f$ is injective. Assume that the rank of $K$ and $V$ is equal to the rank of $K$ and $\mathrm{V'}$. Then the linear equivalence of $f$ is a linear equivalence of $V$ and $\mathrm{V'}$.

basisOfFinrankZerodefMathlib.LinearAlgebra.FiniteDimensional.Basic, 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.FiniteDimensional.Defs

FiniteDimensionaldefMathlib.LinearAlgebra.FiniteDimensional.Defs, predicate

Wording

no wording

English

Let $K$ and $V$ be sets. Then $\mathrm{FiniteDimensional}$ holds for $K$ and $V$, if $\operatorname{Finite}$ holds for $K$ and $V$.

Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

FiniteDimensional.LinearEquiv.quotEquivOfEquivdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

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

English

Let $x_{6}$ be a linear equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {p}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {q}{x_{9}})}$. Let $x_{7}$ be a linear equivalence of $V$ and $x_{3}$. Then the quotient equivalence of $x_{6}$ and $x_{7}$ is a linear equivalence of the set of quotients of $V$ and $p$ and the set of quotients of $x_{3}$ and $q$.

FiniteDimensional.LinearEquiv.quotEquivOfQuotEquivdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

the quotient equivalence of f (from the name)

English

Let $f$ be a linear equivalence of the set of quotients of $V$ and $p$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {q}{x_{4}})}$. Then the quotient equivalence of $f$ is a linear equivalence of the set of quotients of $V$ and $q$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$.

LinearMap.linearEquivOfInjectivedefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

the linear equivalence of f (from the name)

English

Let $f$ be a linear map of $V$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ is injective. Assume that the rank of $K$ and $V$ is equal to the rank of $K$ and $x_{3}$. Then the linear equivalence of $f$ is a linear equivalence of $V$ and $x_{3}$.

basisOfLinearIndependentOfCardEqFinrankdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

the basis of lin_ind and card_eq (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $K$ and $b$. Assume that the cardinality of $x_{3}$ is equal to the rank of $K$ and $V$. Then the basis of $\mathrm{lin\_ind}$ and $\mathrm{card\_eq}$ is a basis of $K$ and $V$.

basisOfLinearIndependentOfCardEqFinrank'defMathlib.LinearAlgebra.FiniteDimensional.Lemmas, 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 $V$ such that $\mathrm{LinearIndependent}$ holds for $K$ and $b$. Assume that the cardinality of $x_{3}$ is equal to the rank of $K$ and $V$. Then the basis of $b$ is a basis of $K$ and $V$.

basisOfPiSpaceOfLinearIndependentdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

the basis of hb (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $K$ and $b$. Then the basis of $\mathrm{hb}$ is a basis of $K$ and the set of functions from elements of $x_{1}$ to elements of $K$.

finsetBasisOfLinearIndependentOfCardEqFinrankdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

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

English

Assume that $s$ is nonempty. Assume that $\mathrm{LinearIndependent}$ holds for $K$ and the function that maps $x_{4}$ to $\MembershipmemMACRoT {s}{x_{4}}$. Assume that the cardinality of $s$ is equal to the rank of $K$ and $V$. Then the finite set basis of $\mathrm{lin\_ind}$ and $\mathrm{card\_eq}$ is a basis of $K$ and $V$.

setBasisOfLinearIndependentOfCardEqFinrankdefMathlib.LinearAlgebra.FiniteDimensional.Lemmas, function or constant

Wording

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

English

Assume that $\mathrm{LinearIndependent}$ holds for $K$ and the function that maps $x_{4}$ to $\MembershipmemMACRoT {s}{x_{4}}$. Assume that the cardinality of the finite set of $s$ is equal to the rank of $K$ and $V$. Then the set basis of $\mathrm{lin\_ind}$ and $\mathrm{card\_eq}$ is a basis of $K$ and $V$.

Mathlib.LinearAlgebra.Finsupp.Defs

Finsupp.curryLinearEquivdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the curry linear equivalence of R (from the name)

English

Let $R$ be a set. Then the curry linear equivalence of $R$ is a linear equivalence of $\FinsuppMACRoQ {\mathrm{Prod} (x , x_{1})}{M}$ and $\FinsuppMACRoQ {x}{(\FinsuppMACRoQ {x_{1}}{M})}$.

Finsupp.lapplydefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{lapply}$ applied to $a$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and $M$.

Finsupp.lcomapDomaindefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $f$ be an injective function from elements of $x$ to elements of $x_{4}$. Then $\operatorname{lcomapDomain}$ applied to $f$ and $\mathrm{hf}$ is a linear map of $\FinsuppMACRoQ {x_{4}}{M}$ and $\FinsuppMACRoQ {x}{M}$.

Finsupp.linearEquivFunOnFinitedefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $R$, $M$ and $x$ be sets. Then $\operatorname{linearEquivFunOnFinite}$ applied to $R$, $M$ and $x$ is a linear equivalence of $\FinsuppMACRoQ {x}{M}$ and the set of functions from elements of $x$ to elements of $M$.

Finsupp.lmapDomaindefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $M$ and $R$ be sets. Let $f$ be a function from elements of $x$ to elements of $x_{4}$. Then $\operatorname{lmapDomain}$ applied to $M$, $R$ and $f$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{4}}{M}$.

Finsupp.lsingledefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $a$ be an element of $x$. Then $\operatorname{lsingle}$ applied to $a$ is a linear map of $M$ and $\FinsuppMACRoQ {x}{M}$.

Finsupp.lsubtypeDomaindefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\operatorname{lsubtypeDomain}$ applied to $s$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and the set of finitely supported functions from the set of elements of $s$ to $M$.

Finsupp.mapDomain.linearEquivdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the linear equivalence of f (from the name)

English

Let $M$ and $R$ be sets. Let $f$ be an equivalence from $x$ to $x_{4}$. Then the linear equivalence of $f$ is a linear equivalence of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x_{4}}{M}$.

Finsupp.mapRange.linearEquivdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the linear equivalence of e (from the name)

English

Let $e$ be a linear equivalence of $M$ and $N$. Then the linear equivalence of $e$ is a linear equivalence of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{N}$.

Finsupp.mapRange.linearMapdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the linear map of f (from the name)

English

Let $f$ be a linear map of $M$ and $N$. Then the linear map of $f$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{N}$.

Module.End.ringEquivEndFinsuppdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the ring isomorphism end finitely supported function of i (from the name)

English

Let $i$ be an element of $x$. Then the ring isomorphism end finitely supported function of $i$ is a ring isomorphism of the set of ends of the set of ends of $R$ and $M$ and $M$ and the set of ends of the set of ends of $R$ and $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{M}$.

Module.End.ringHomEndFinsuppdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the ring homomorphism end finitely supported function of x (from the name)

English

Let $x$ be a set. Then the ring homomorphism end finitely supported function of $x$ is a ring homomorphism of the set of ends of the set of ends of $R$ and $M$ and $M$ and the set of ends of the set of ends of $R$ and $\FinsuppMACRoQ {x}{M}$ and $\FinsuppMACRoQ {x}{M}$.

Module.subsingletonEquivdefMathlib.LinearAlgebra.Finsupp.Defs, function or constant

Wording

the subsingleton equivalence of M and x (from the name)

English

Let $R$, $M$ and $x$ be sets. Then the subsingleton equivalence of $M$ and $x$ is a linear equivalence of $M$ and $\FinsuppMACRoQ {x}{R}$.

Mathlib.LinearAlgebra.Finsupp.LSum

Finsupp.domLCongrdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

the domain congruence of e (from the name)

English

Let $e$ be an equivalence from $x_{3}$ to $x_{4}$. Then the domain congruence of $e$ is a linear equivalence of $\FinsuppMACRoQ {x_{3}}{M}$ and $\FinsuppMACRoQ {x_{4}}{M}$.

Finsupp.lcongrdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

no wording

English

Let $x_{11}$ be an equivalence from $x_{9}$ to $x_{10}$. Let $x_{12}$ be a linear equivalence of $M$ and $N$. Then $\operatorname{lcongr}$ applied to $x_{11}$ and $x_{12}$ is a linear equivalence of $\FinsuppMACRoQ {x_{9}}{M}$ and $\FinsuppMACRoQ {x_{10}}{N}$ defined as the composition of the domain congruence of $x_{11}$ and the linear equivalence of $x_{12}$.

Finsupp.liftdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

the lift of R and X (from the name)

English

Let $M$, $R$ and $X$ be sets. Then the lift of $R$ and $X$ is an additive equivalence of the set of functions from elements of $X$ to elements of $M$ and the set of linear maps of $\FinsuppMACRoQ {X}{R}$ and $M$ defined as the composition of the arrow congruence of the identity of $X$ and the inverse of the additive equivalence of $\operatorname{ringLmapEquivSelf}$ applied to $R$, $\Natural$ and $M$ and the additive equivalence of $\operatorname{lsum}$ applied to $\Natural$.

Finsupp.lliftdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

no wording

English

Let $M$, $R$, $S$ and $X$ be sets. Then $\operatorname{llift}$ applied to $M$, $R$, $S$ and $X$ is a linear equivalence of the set of functions from elements of $X$ to elements of $M$ and the set of linear maps of $\FinsuppMACRoQ {X}{R}$ and $M$.

Finsupp.lsumdefMathlib.LinearAlgebra.Finsupp.LSum, 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 of $x$ to linear maps of $M$ and $N$ and the set of linear maps of $\FinsuppMACRoQ {x}{M}$ and $N$.

LinearMap.splittingOfFinsuppSurjectivedefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

the splitting of f and s (from the name)

English

Let $f$ be a linear map of $M$ and $\FinsuppMACRoQ {x_{3}}{R}$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the splitting of $f$ and $s$ is a linear map of $\FinsuppMACRoQ {x_{3}}{R}$ and $M$.

Submodule.mulLeftMapdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

the multiplicative left map of N and m (from the name)

English

Let $N$ be a submodule of $R$ and $S$. Let $m$ be a function from elements of $x_{3}$ to elements of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {M}{x_{6}})}$. Then the multiplicative left map of $N$ and $m$ is a linear map of $\FinsuppMACRoQ {x_{3}}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})})}$ and $S$ defined as $\operatorname{lsum}$ applied to $R$ and the function that maps $i_{1}$ to $\HSMulhSMulMACRoAL {m (i_{1})}{\operatorname{subtype} (N)}$.

Submodule.mulRightMapdefMathlib.LinearAlgebra.Finsupp.LSum, function or constant

Wording

the multiplicative right map of M and n (from the name)

English

Let $M$ be a submodule of $R$ and $S$. Let $n$ be a function from elements of $x_{3}$ to elements of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {N}{x_{6}})}$. Then the multiplicative right map of $M$ and $n$ is a linear map of $\FinsuppMACRoQ {x_{3}}{(\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {M}{x_{4}})})}$ and $S$ defined as $\operatorname{lsum}$ applied to $R$ and the function that maps $i_{1}$ to $\HSMulhSMulMACRoAL {\operatorname{op} (n (i_{1}))}{\operatorname{subtype} (M)}$.

Mathlib.LinearAlgebra.Finsupp.LinearCombination

Finsupp.addSingleEquivdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the additive single equivalence of i and c (from the name)

English

Let $i$ be an element of $x$. Let $c$ be a function from elements of $x$ to elements of $R$ such that $\EqtMACRoH {c (i)}{0}$. Then the additive single equivalence of $i$ and $c$ is a linear equivalence of $\FinsuppMACRoQ {x}{R}$ and $\FinsuppMACRoQ {x}{R}$.

Finsupp.bilinearCombinationdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the bilinear combination of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the bilinear combination of $R$ and $S$ is a linear map of the set of functions from elements of $x$ to elements of $M$ and the set of linear maps of $\FinsuppMACRoQ {x}{R}$ and $M$.

Finsupp.linearCombinationdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the linear combination of R and v (from the name)

English

Let $R$ be a set. Let $v$ be a function from elements of $x$ to elements of $M$. Then the linear combination of $R$ and $v$ is a linear map of $\FinsuppMACRoQ {x}{R}$ and $M$ defined as $\operatorname{lsum}$ applied to $\Natural$ and the function that maps $i_{1}$ to the right scalar multiple of the identity and $v$ applied to $i_{1}$.

Finsupp.linearCombinationOndefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

no wording

English

Let $x$, $M$ and $R$ be sets. Let $v$ be a function from elements of $x$ to elements of $M$. Let $s$ be an element of $\wp x$. Then $\operatorname{linearCombinationOn}$ applied to $x$, $M$, $R$, $v$ and $s$ is a linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{supported} (R , R , s)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{image} (v , s))}{x_{5}})}$.

Fintype.bilinearCombinationdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the bilinear combination of R and S (from the name)

English

Let $R$ and $S$ be sets. Then the bilinear combination of $R$ and $S$ is a linear map of the set of functions from elements of $x$ to elements of $M$ and the set of linear maps of the set of functions from elements of $x$ to elements of $R$ and $M$.

Fintype.linearCombinationdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the linear combination of R and v (from the name)

English

Let $R$ be a set. Let $v$ be a function from elements of $x$ to elements of $M$. Then the linear combination of $R$ and $v$ is a linear map of the set of functions from elements of $x$ to elements of $R$ and $M$.

Span.reprdefMathlib.LinearAlgebra.Finsupp.LinearCombination, function or constant

Wording

the representation of w and x3 (from the name)

English

Let $R$ be a set. Let $w$ be an element of $\wp M$. Let $x_{3}$ be an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , w)}{x_{4}})}$. Then the representation of $w$ and $x_{3}$ is an element of $\FinsuppMACRoQ {\operatorname{Elem} (w)}{R}$ defined as $\operatorname{proj0}$ applied to $\mathrm{wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_Finsupp\_\_LinearCombination\_\_859253174\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$, $w$ and $x_{3}$.

Mathlib.LinearAlgebra.Finsupp.Pi

Finsupp.lcoeFundefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

no wording

English

$\operatorname{lcoeFun}$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and the set of functions from elements of $x$ to elements of $M$.

Finsupp.submoduledefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the submodule of S (from the name)

English

Let $S$ be a function from elements of $x_{3}$ to submodules of $R$ and $M$. Then the submodule of $S$ is a submodule of $R$ and $\FinsuppMACRoQ {x_{3}}{M}$.

Finsupp.uniqueLinearEquivdefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the unique linear equivalence of a (from the name)

English

Let $R$ and $M$ be sets. Let $a$ be an element of $x$. Then the unique linear equivalence of $a$ is a linear equivalence of $\FinsuppMACRoQ {x}{M}$ and $M$.

FunOnFinite.linearMapdefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the linear map of f (from the name)

English

Let $R$ and $M$ be sets. Let $f$ be a function from elements of $X$ to elements of $Y$. Then the linear map of $f$ is a linear map of the set of functions from elements of $X$ to elements of $M$ and the set of functions from elements of $Y$ to elements of $M$ defined as the composition of the composition of $\operatorname{toLinearMap}$ applied to $\operatorname{linearEquivFunOnFinite}$ applied to $R$, $M$ and $Y$ and $\operatorname{lmapDomain}$ applied to $M$, $R$ and $f$ and $\operatorname{toLinearMap}$ applied to the inverse of $\operatorname{linearEquivFunOnFinite}$ applied to $R$, $M$ and $X$.

FunOnFinite.mapdefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the map of s and x1 (from the name)

English

Let $f$ be a function from elements of $X$ to elements of $Y$. Let $s$ be a function from elements of $X$ to elements of $M$. Let $x_{1}$ be an element of $Y$. Then the map of $s$ and $x_{1}$ is an element of $M$ defined as $\operatorname{equivFunOnFinite}$ applied to the map domain of $f$ and $\operatorname{symm}$ applied to $\operatorname{equivFunOnFinite}$ and $s$ and $x_{1}$.

LinearMap.prodOfFinsuppNatdefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the product of f (from the name)

English

Let $f$ be a linear map of $\mathrm{Prod}$ applied to $P$ and $M$ and $M$. Then the product of $f$ is a linear map of $\FinsuppMACRoQ {\Natural}{P}$ and $\mathrm{Prod}$ applied to $P$ and $M$ defined as $\operatorname{lsum}$ applied to $\Natural$ and the function that maps $n_{1}$ to the composition of the exponentiation of the composition of the right injection of $P$ and $M$ and $f$ to $n_{1}$ and the left injection of $P$ and $M$.

LinearMap.splittingOfFunOnFintypeSurjectivedefMathlib.LinearAlgebra.Finsupp.Pi, function or constant

Wording

the splitting of f and s (from the name)

English

Let $f$ be a linear map of $M$ and the set of functions from elements of $x_{3}$ to elements of $R$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the splitting of $f$ and $s$ is a linear map of the set of functions from elements of $x_{3}$ to elements of $R$ and $M$.

Mathlib.LinearAlgebra.Finsupp.SumProd

Finsupp.sigmaFinsuppLEquivPiFinsuppdefMathlib.LinearAlgebra.Finsupp.SumProd, function or constant

Wording

the sigma finitely supported function equivalence product finitely supported function of R (from the name)

English

Let $R$ be a set. Then the sigma finitely supported function equivalence product finitely supported function of $R$ is a linear equivalence of $\FinsuppMACRoQ {\Sigma (\lambda j . x_{3} (j))}{M}$ and the set of functions from elements $j_{1}$ of $x_{1}$ to elements of $\FinsuppMACRoQ {x_{3} (j_{1})}{M}$.

Finsupp.sumFinsuppLEquivProdFinsuppdefMathlib.LinearAlgebra.Finsupp.SumProd, function or constant

Wording

the sum finitely supported function equivalence product finitely supported function of R (from the name)

English

Let $R$ be a set. Then the sum finitely supported function equivalence product finitely supported function of $R$ is a linear equivalence of $\FinsuppMACRoQ {\mathrm{Sum} (x_{3} , x_{4})}{M}$ and $\mathrm{Prod}$ applied to $\FinsuppMACRoQ {x_{3}}{M}$ and $\FinsuppMACRoQ {x_{4}}{M}$.

Mathlib.LinearAlgebra.Finsupp.Supported

Finsupp.congrdefMathlib.LinearAlgebra.Finsupp.Supported, function or constant

Wording

the congruence of t and e (from the name)

English

Let $s$ be an element of $\wp x$. Let $t$ be an element of $\wp x_{4}$. Let $e$ be an equivalence from the set of elements of $s$ to the set of elements of $t$. Then the congruence of $t$ and $e$ is a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{supported} (M , R , s)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{supported} (M , R , t)}{x_{6}})}$ defined as the composition of $\operatorname{supportedEquivFinsupp}$ applied to $s$ and the composition of the domain congruence of $e$ and the inverse of $\operatorname{supportedEquivFinsupp}$ applied to $t$.

Finsupp.restrictDomdefMathlib.LinearAlgebra.Finsupp.Supported, function or constant

Wording

no wording

English

Let $M$ and $R$ be sets. Let $s$ be an element of $\wp x$. Then $\operatorname{restrictDom}$ applied to $M$, $R$ and $s$ is a linear map of $\FinsuppMACRoQ {x}{M}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{supported} (M , R , s)}{x_{5}})}$.

Finsupp.supporteddefMathlib.LinearAlgebra.Finsupp.Supported, function or constant

Wording

no wording

English

Let $M$ and $R$ be sets. Let $s$ be an element of $\wp x$. Then $\operatorname{supported}$ applied to $M$, $R$ and $s$ is a submodule of $R$ and $\FinsuppMACRoQ {x}{M}$.

Finsupp.supportedEquivFinsuppdefMathlib.LinearAlgebra.Finsupp.Supported, function or constant

Wording

no wording

English

Let $s$ be an element of $\wp x$. Then $\operatorname{supportedEquivFinsupp}$ applied to $s$ is a linear equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{supported} (M , R , s)}{x_{4}})}$ and the set of finitely supported functions from the set of elements of $s$ to $M$.

Mathlib.LinearAlgebra.Finsupp.VectorSpace

DFinsupp.basisdefMathlib.LinearAlgebra.Finsupp.VectorSpace, function or constant

Wording

the basis of b (from the name)

English

Let $b$ be a function from elements $i_{2}$ of $x$ to bases of $R$ and $M$ applied to $i_{2}$. Then the basis of $i_{2}$ is a basis of $R$ and the set of finitely supported functions of the function that maps $i_{1}$ to $M$ applied to $i_{1}$ defined as the function that maps $b$ to $\operatorname{ofRepr}$ applied to the composition of the linear equivalence of the function that maps $i$ to the representation of $i_{2}$ applied to $i$ and the inverse of the sigma finitely supported function linear equivalence finitely supported function of $R$ and $b$.

Finsupp.basisdefMathlib.LinearAlgebra.Finsupp.VectorSpace, function or constant

Wording

the basis of b (from the name)

English

Let $b$ be a function from elements $i_{1}$ of $x$ to bases of $R$ and $M$. Then the basis of $i_{1}$ is a basis of $R$ and $\FinsuppMACRoQ {x}{M}$ defined as the function that maps $b$ to $\operatorname{ofRepr}$ applied to the composition of the finitely supported function linear equivalence finitely supported function of $R$ and the composition of the linear equivalence of the function that maps $i$ to the representation of $i_{1}$ applied to $i$ and the inverse of the sigma finitely supported function linear equivalence finitely supported function of $R$ and $b$.

Finsupp.basisSingleOnedefMathlib.LinearAlgebra.Finsupp.VectorSpace, function or constant

Wording

the basis single one (from the name)

English

The basis single one is a basis of $R$ and $\FinsuppMACRoQ {x}{R}$ defined as $\operatorname{ofRepr}$ applied to the identity map of $R$ and $\FinsuppMACRoQ {x}{R}$.

Mathlib.LinearAlgebra.FixedSubmodule

LinearEquiv.fixedReducedefMathlib.LinearAlgebra.FixedSubmodule, function or constant

Wording

no wording

English

Let $e$ be a linear equivalence of $V$ and $V$. Then $\operatorname{fixedReduce}$ applied to $e$ is a linear equivalence of the set of quotients of $V$ and the fixed submodule of $\operatorname{toLinearMap}$ applied to $e$ and the set of quotients of $V$ and the fixed submodule of $\operatorname{toLinearMap}$ applied to $e$ defined as $\operatorname{reduce}$ applied to the fixed submodule of $\operatorname{toLinearMap}$ applied to $e$ and $e$.

LinearEquiv.reducedefMathlib.LinearAlgebra.FixedSubmodule, function or constant

Wording

no wording

English

Let $W$ be a submodule of $R$ and $V$. Then $\operatorname{reduce}$ applied to $W$ is a monoid homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{stabilizer} (\mathrm{LinearEquiv} (V , V), W)}{x_{3}})}$ and the set of linear equivalences of the set of quotients of $V$ and $W$ and the set of quotients of $V$ and $W$.

LinearMap.fixedSubmoduledefMathlib.LinearAlgebra.FixedSubmodule, function or constant

Wording

the fixed submodule of f (from the docstring)

English

Let $f$ be a linear map of $V$ and $V$. Then the fixed submodule of $f$ is a submodule of $R$ and $V$.

Mathlib.LinearAlgebra.FreeAlgebra

FreeAlgebra.basisFreeMonoiddefMathlib.LinearAlgebra.FreeAlgebra, function or constant

Wording

the basis free monoid of R and X (from the name)

English

Let $R$ and $X$ be sets. Then the basis free monoid of $R$ and $X$ is a basis of $R$ and the set of free algebras of $R$ and $X$ defined as the map of the basis single one and the inverse of the composition of the linear equivalence of the equivalence monoid algebra free monoid and the coefficient linear equivalence of $R$.

Mathlib.LinearAlgebra.FreeModule.Basic

Module.FreeclassMathlib.LinearAlgebra.FreeModule.Basic, predicate

Wording

no wording

English

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

Module.Free.ChooseBasisIndexdefMathlib.LinearAlgebra.FreeModule.Basic, type

Wording

no wording

English

Let $R$ and $M$ be sets. Then the elements of $\operatorname{ChooseBasisIndex}$ applied to $R$ and $M$ are a basic type.

Module.Free.chooseBasisdefMathlib.LinearAlgebra.FreeModule.Basic, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\operatorname{chooseBasis}$ applied to $R$ and $M$ is a basis of $R$ and $M$.

Module.Free.constrdefMathlib.LinearAlgebra.FreeModule.Basic, function or constant

Wording

no wording

English

Let $R$, $M$ and $N$ be sets. Then $\operatorname{constr}$ applied to $R$, $M$ and $N$ is a linear equivalence of the set of functions from elements of $\operatorname{ChooseBasisIndex}$ applied to $R$ and $M$ to elements of $N$ and the set of linear maps of $M$ and $N$ defined as $\operatorname{constr}$ applied to $\operatorname{chooseBasis}$ applied to $R$ and $M$ and $S$.

Mathlib.LinearAlgebra.FreeModule.Finite.Quotient

Submodule.quotientEquivDirectSumdefMathlib.LinearAlgebra.FreeModule.Finite.Quotient, function or constant

Wording

the quotient equivalence direct sum of b (from the name)

English

Let $F$ be a set. Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {N}{x_{7}})}$ is equal to the rank of $R$ and $M$. Then the quotient equivalence direct sum of $b$ is a linear equivalence of the set of quotients of $M$ and $N$ and the set of direct sums of $x$ and the function that maps $i$ to the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{smithNormalFormCoeffs}$ applied to $b$, $h_{4}$ and $i$ defined as the composition of $\operatorname{restrictScalars}$ applied to $F$ and the quotient equivalence product span of $N$ and $b$ and the inverse of the linear equivalence function on finite type of the function that maps $i$ to the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{smithNormalFormCoeffs}$ applied to $b$, $h_{4}$ and $i$.

Submodule.quotientEquivPiSpandefMathlib.LinearAlgebra.FreeModule.Finite.Quotient, function or constant

Wording

the quotient equivalence product span of N and b (from the name)

English

Let $N$ be a submodule of $R$ and $M$. Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ is equal to the rank of $R$ and $M$. Then the quotient equivalence product span of $N$ and $b$ is a linear equivalence of the set of quotients of $M$ and $N$ and the set of functions from elements $i$ of $x$ to quotients of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{smithNormalFormCoeffs}$ applied to $b$, $h_{3}$ and $i$.

Submodule.quotientEquivPiZModdefMathlib.LinearAlgebra.FreeModule.Finite.Quotient, function or constant

Wording

no wording

English

Let $N$ be a submodule of $\Integer$ and $M$. Let $b$ be a basis of $\Integer$ and $M$. Assume that the rank of $\Integer$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {N}{x_{2}})}$ is equal to the rank of $\Integer$ and $M$. Then $\operatorname{quotientEquivPiZMod}$ applied to $N$, $b$ and $h_{1}$ is an additive equivalence of the set of quotients of $M$ and $N$ and the set of functions from elements $i$ of $x$ to elements of $\mathrm{ZMod}$ applied to $\IntnatAbsMACRoY {\operatorname{smithNormalFormCoeffs} (b , h_{1} , i)}$ defined as the composition of the additive equivalence of the quotient equivalence product span of $N$ and $b$ and the right product congruence of the function that maps $i$ to the additive equivalence of $\operatorname{quotientSpanEquivZMod}$ applied to $\operatorname{smithNormalFormCoeffs}$ applied to $b$, $h_{1}$ and $i$.

Mathlib.LinearAlgebra.FreeModule.IdealQuotient

Ideal.quotientEquivDirectSumdefMathlib.LinearAlgebra.FreeModule.IdealQuotient, function or constant

Wording

the quotient equivalence direct sum of b (from the name)

English

Let $F$ be a set. Let $b$ be a basis of $R$ and $S$. Assume that $I$ is distinct from the bottom. Then the quotient equivalence direct sum of $b$ is a linear equivalence of the set of quotients of $S$ and $I$ and the set of direct sums of $x$ and the function that maps $i$ to the set of quotients of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{smithCoeffs}$ applied to $b$, $I$, $\mathrm{hI}$ and $i$ defined as the quotient equivalence direct sum of $b$.

Ideal.quotientEquivPiSpandefMathlib.LinearAlgebra.FreeModule.IdealQuotient, function or constant

Wording

the quotient equivalence product span of I and b (from the name)

English

Let $I$ be an ideal of $S$. Let $b$ be a basis of $R$ and $S$. Assume that $I$ is distinct from the bottom. Then the quotient equivalence product span of $I$ and $b$ is a linear equivalence of the set of quotients of $S$ and $I$ and the set of functions from elements $i$ of $x$ to quotients of $R$ and the span of $\operatorname{singleton}$ applied to $\operatorname{smithCoeffs}$ applied to $b$, $I$, $\mathrm{hI}$ and $i$ defined as the quotient equivalence product span of $\operatorname{restrictScalars}$ applied to $R$ and $I$ and $b$.

Ideal.quotientEquivPiZModdefMathlib.LinearAlgebra.FreeModule.IdealQuotient, function or constant

Wording

no wording

English

Let $I$ be an ideal of $S$. Let $b$ be a basis of $\Integer$ and $S$. Assume that $I$ is distinct from the bottom. Then $\operatorname{quotientEquivPiZMod}$ applied to $I$, $b$ and $\mathrm{hI}$ is an additive equivalence of the set of quotients of $S$ and $I$ and the set of functions from elements $i$ of $x$ to elements of $\mathrm{ZMod}$ applied to $\IntnatAbsMACRoY {\operatorname{smithCoeffs} (b , I , \mathrm{hI} , i)}$.

Mathlib.LinearAlgebra.FreeModule.ModN

ModNdefMathlib.LinearAlgebra.FreeModule.ModN, type

Wording

no wording

English

Let $G$ be a set. Let $n$ be a natural number. Then an element of $\mathrm{ModN}$ applied to $G$ and $n$ is an element of the function that maps $G$ and $n$ to the set of quotients of $G$ and the range of $\operatorname{lsmul}$ applied to $\Integer$, $G$ and $n$.

ModN.basisdefMathlib.LinearAlgebra.FreeModule.ModN, function or constant

Wording

the basis of b (from the name)

English

Let $b$ be a basis of $\Integer$ and $G$. Then the basis of $b$ is a basis of $\mathrm{ZMod}$ applied to $n$ and $\mathrm{ModN}$ applied to $G$ and $n$.

ModN.liftEquivdefMathlib.LinearAlgebra.FreeModule.ModN, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an equivalence from the set of additive monoid homomorphisms of $\mathrm{ModN}$ applied to $G$ and $n$ and $M$ to $\SubtypeSet {x_{2}}{\mathrm{forall} (G , \lambda g . \EqtMACRoH {(\HSMulhSMulMACRoAL {n}{x_{2} (g)})}{0})}$.

ModN.liftEquiv'defMathlib.LinearAlgebra.FreeModule.ModN, function or constant

Wording

the lift equivalence (from the name)

English

The lift equivalence is an equivalence from the set of linear maps of $\mathrm{ModN}$ applied to $G$ and $n$ and $H$ to $\SubtypeSet {x_{3}}{\mathrm{forall} (G , \lambda g . \EqtMACRoH {(\HSMulhSMulMACRoAL {n}{x_{3} (g)})}{0})}$ defined as the composition of $\operatorname{toEquiv}$ applied to the inverse of $\operatorname{toZModLinearMapEquiv}$ applied to $n$ and the lift equivalence.

ModN.mkQdefMathlib.LinearAlgebra.FreeModule.ModN, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{mkQ}$ applied to $n$ is an additive monoid homomorphism of $G$ and $\mathrm{ModN}$ applied to $G$ and $n$ defined as the additive monoid homomorphism of $\operatorname{mkQ}$ applied to the range of $\operatorname{lsmul}$ applied to $\Integer$, $G$ and $n$.

Mathlib.LinearAlgebra.FreeModule.PID

Ideal.ringBasisdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the ring basis of b and I (from the name)

English

Let $b$ be a basis of $R$ and $S$. Let $I$ be an ideal of $S$ such that $I$ is distinct from the bottom. Then the ring basis of $b$ and $I$ is a basis of $R$ and $S$ defined as $\operatorname{choose}$ applied to $\mathrm{Ideal\_\_exists\_smith\_normal\_form}$ applied to $b$, $I$ and $\mathrm{hI}$.

Ideal.selfBasisdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the self basis of b and I (from the name)

English

Let $b$ be a basis of $R$ and $S$. Let $I$ be an ideal of $S$ such that $I$ is distinct from the bottom. Then the self basis of $b$ and $I$ is a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {I}{x_{4}})}$.

Ideal.smithCoeffsdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $S$. Let $I$ be an ideal of $S$ such that $I$ is distinct from the bottom. Let $x_{4}$ be an element of $x$. Then $\operatorname{smithCoeffs}$ applied to $b$, $I$, $\mathrm{hI}$ and $x_{4}$ is an element of $R$.

Ideal.smithNormalFormdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form of b and I (from the name)

English

Let $b$ be a basis of $R$ and $S$. Let $I$ be an ideal of $S$ such that $I$ is distinct from the bottom. Then the Smith normal form of $b$ and $I$ is a Smith normal form of $x$ and the cardinality of $x$.

Module.Basis.SmithNormalFormstructureMathlib.LinearAlgebra.FreeModule.PID, type

Wording

Smith normal form of x3 and n (from the name)

English

Let $N$ be a submodule of $R$ and $M$. Let $x_{3}$ be a set. Let $n$ be a natural number. Then the Smith normal forms of $x_{3}$ and $n$ are a basic type.

Module.Basis.SmithNormalForm.adefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Smith normal form of $x_{3}$ and $n$. Let $x_{4}$ be an element of $\mathrm{Fin}$ applied to $n$. Then $\operatorname{a}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $R$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{4}$.

Module.Basis.SmithNormalForm.bMdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Smith normal form of $x_{3}$ and $n$. Then $\operatorname{bM}$ applied to $\mathrm{self}$ is a basis of $R$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Module.Basis.SmithNormalForm.bNdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Smith normal form of $x_{3}$ and $n$. Then $\operatorname{bN}$ applied to $\mathrm{self}$ is a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

Module.Basis.SmithNormalForm.fdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a Smith normal form of $x_{3}$ and $n$. Then $\operatorname{f}$ applied to $\mathrm{self}$ is an embedding of $\mathrm{Fin}$ applied to $n$ and $x_{3}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

Module.basisOfFiniteTypeTorsionFreedefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the basis of hs (from the name)

English

Assume that the span of $R$ and the range of $s$ is equal to the top. Then the basis of $\mathrm{hs}$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bases of $R$ and $M$.

Module.basisOfFiniteTypeTorsionFree'defMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the basis (from the name)

English

The basis is an element of $\Sigma$ applied to the function that maps $n$ to the set of bases of $R$ and $M$.

Submodule.basisOfPiddefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the basis of b and N (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $N$ be a submodule of $R$ and $M$. Then the basis of $b$ and $N$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bases of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$.

Submodule.basisOfPidOfLEdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the basis of hNO and b (from the name)

English

Assume that $N \leq O$. Let $b$ be a basis of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {O}{x_{5}})}$. Then the basis of $\mathrm{hNO}$ and $b$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bases of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$.

Submodule.basisOfPidOfLESpandefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the basis of hb and le (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $b$. Assume that $N$ is less than or equal to the span of $R$ and the range of $b$. Then the basis of $\mathrm{hb}$ and $\mathrm{le}$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of bases of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ defined as the basis of $\mathrm{le}$ and the span of $\mathrm{hb}$.

Submodule.smithNormalFormdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form of b and N (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $N$ be a submodule of $R$ and $M$. Then the Smith normal form of $b$ and $N$ is an element of $\Sigma$ applied to the function that maps $n$ to the set of Smith normal forms of $x$ and $n$.

Submodule.smithNormalFormBotBasisdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form bottom basis of b and h3 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$ is equal to the rank of $R$ and $M$. Then the Smith normal form bottom basis of $b$ and $h_{3}$ is a basis of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$.

Submodule.smithNormalFormCoeffsdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$ is equal to the rank of $R$ and $M$. Let $x_{4}$ be an element of $x$. Then $\operatorname{smithNormalFormCoeffs}$ applied to $b$, $h_{3}$ and $x_{4}$ is an element of $R$.

Submodule.smithNormalFormOfLEdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form of N and O (from the name)

English

Let $b$ be a basis of $R$ and $M$. Let $N$ and $O$ be submodules of $R$ and $M$ such that $N \leq O$. Then the Smith normal form of $N$ and $O$ is an element of $\Sigma$ applied to the function that maps $o$ to $\Sigma$ applied to the function that maps $n$ to the set of Smith normal forms of $\mathrm{Fin}$ applied to $o$ and $n$.

Submodule.smithNormalFormOfRankEqdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form of b and h2 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$ is equal to the rank of $R$ and $M$. Then the Smith normal form of $b$ and $h_{2}$ is a Smith normal form of $x$ and the cardinality of $x$.

Submodule.smithNormalFormTopBasisdefMathlib.LinearAlgebra.FreeModule.PID, function or constant

Wording

the Smith normal form top basis of b and h3 (from the name)

English

Let $b$ be a basis of $R$ and $M$. Assume that the rank of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ is equal to the rank of $R$ and $M$. Then the Smith normal form top basis of $b$ and $h_{3}$ is a basis of $R$ and $M$ defined as $\operatorname{choose}$ applied to $\mathrm{Submodule\_\_exists\_smith\_normal\_form\_of\_rank\_eq}$ applied to $b$ and $h_{3}$.

Mathlib.LinearAlgebra.FreeProduct.Basic

LinearAlgebra.FreeProductdefMathlib.LinearAlgebra.FreeProduct.Basic, type

Wording

free product of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then a free product of $R$ and $A$ is an element of the function that maps $R$ and $A$ to the set of quotients of the ring congruence relation of $R$ and $A$.

LinearAlgebra.FreeProduct.FreeTensorAlgebradefMathlib.LinearAlgebra.FreeProduct.Basic, type

Wording

free tensor algebra of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then a free tensor algebra of $R$ and $A$ is an element of the function that maps $R$ and $A$ to the set of tensor algebras of $R$ and the set of direct sums of $I$ and the function that maps $i$ to $A$ applied to $i$.

LinearAlgebra.FreeProduct.PowerAlgebradefMathlib.LinearAlgebra.FreeProduct.Basic, type

Wording

power algebra of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then a power algebra of $R$ and $A$ is an element of the function that maps $R$ and $A$ to the set of direct sums of $\Natural$ and the function that maps $n$ to the set of tensor powers of $n$ and the set of direct sums of $I$ and the function that maps $i$ to $A$ applied to $i$.

LinearAlgebra.FreeProduct.asPowersdefMathlib.LinearAlgebra.FreeProduct.Basic, type

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then an element of $\operatorname{asPowers}$ applied to $R$ and $A$ is an element of the function that maps $R$ and $A$ to the set of quotients of the ring congruence relation of $R$ and $A$.

LinearAlgebra.FreeProduct.asPowersEquivdefMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then $\operatorname{asPowersEquiv}$ applied to $R$ and $A$ is an algebra isomorphism of $\operatorname{asPowers}$ applied to $R$ and $A$ and the set of free products of $R$ and $A$.

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

Wording

the lift of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the lift of $R$ and $A$ is an equivalence from the set of functions from elements $i$ of $I$ to algebra homomorphisms of $A$ applied to $i$ and $B$ to the set of algebra homomorphisms of the set of free products of $R$ and $A$ and $B$.

LinearAlgebra.FreeProduct.lofdefMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then $\operatorname{lof}$ applied to $R$, $A$ and $i$ is a linear map of $A$ applied to $i$ and the set of free products of $R$ and $A$ defined as the composition of the inclusion of $R$ and $A$ and $\operatorname{lof}$ applied to $R$, $I$, $A$ and $i$.

LinearAlgebra.FreeProduct.mkAlgHomdefMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

the algebra homomorphism of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the algebra homomorphism of $R$ and $A$ is an algebra homomorphism of the set of free tensor algebras of $R$ and $A$ and the set of free products of $R$ and $A$ defined as $\mathrm{RingCon\_\_mk\_u2090\_}$ applied to $R$ and the ring congruence relation of $R$ and $A$.

LinearAlgebra.FreeProduct.ofdefMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then $\operatorname{of}$ applied to $R$ and $A$ is an algebra homomorphism of $A$ applied to $i$ and the set of free products of $R$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{LinearAlgebra\_\_FreeProduct\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_FreeProduct\_\_Basic\_\_376873978\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$ and $A$.

LinearAlgebra.FreeProduct.powerAlgebraEquivFreeTensorAlgebradefMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

the power algebra equivalence free tensor algebra of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the power algebra equivalence free tensor algebra of $R$ and $A$ is an algebra isomorphism of the set of power algebras of $R$ and $A$ and the set of free tensor algebras of $R$ and $A$ defined as the inverse of the equivalence direct sum.

LinearAlgebra.FreeProduct.relinductiveMathlib.LinearAlgebra.FreeProduct.Basic, predicate

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Let $x_{4}$ and $x_{5}$ be free tensor algebras of $R$ and $A$. Then we can say that $\operatorname{rel}$ holds for $R$, $A$, $x_{4}$ and $x_{5}$.

LinearAlgebra.FreeProduct.rel'defMathlib.LinearAlgebra.FreeProduct.Basic, predicate

Wording

no wording

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Let $x_{4}$ be a direct sum of $\Natural$ and the function that maps $n_{1}$ to the set of tensor powers of $n_{1}$ and the set of direct sums of $I$ and the function that maps $i_{1}$ to $A$ applied to $i_{1}$. Let $x_{5}$ be a direct sum of $\Natural$ and the function that maps $n$ to the set of tensor powers of $n$ and the set of direct sums of $I$ and the function that maps $i$ to $A$ applied to $i$. Then $\operatorname{rel'}$ holds for $R$, $A$, $x_{4}$ and $x_{5}$, if $\operatorname{onFun}$ holds for $\operatorname{rel}$ applied to $R$ and $A$, $\operatorname{coe}$ applied to the canonical map, $x_{4}$ and $x_{5}$.

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

Wording

the ring congruence relation of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the ring congruence relation of $R$ and $A$ is a ring congruence relation of the set of free tensor algebras of $R$ and $A$ defined as the ring congruence relation generator of $\operatorname{rel}$ applied to $R$ and $A$.

LinearAlgebra.FreeProduct.ringCon'defMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

the ring congruence relation of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the ring congruence relation of $R$ and $A$ is a ring congruence relation of the set of power algebras of $R$ and $A$ defined as the ring congruence relation generator of $\operatorname{rel'}$ applied to $R$ and $A$.

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

Wording

the inclusion of A and i (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Let $i$ be an element of $I$. Then the inclusion of $A$ and $i$ is an algebra homomorphism of $A$ applied to $i$ and the set of free products of $R$ and $A$ defined as $\operatorname{proj0}$ applied to $\mathrm{LinearAlgebra\_\_FreeProduct\_\_wrapped\_\_\_\_u40\_\_\_Mathlib\_\_LinearAlgebra\_\_FreeProduct\_\_Basic\_\_3867189960\_\_\_hygCtx\_\_\_hyg\_\_2}$, $R$, $A$ and $i$.

LinearAlgebra.FreeProduct.ι'defMathlib.LinearAlgebra.FreeProduct.Basic, function or constant

Wording

the inclusion of R and A (from the name)

English

Let $R$ be a set. Let $A$ be a function from elements of $I$ to sets. Then the inclusion of $R$ and $A$ is a linear map of the set of direct sums of $I$ and the function that maps $i$ to $A$ applied to $i$ and the set of free products of $R$ and $A$ defined as the composition of the linear map of the algebra homomorphism of $R$ and $A$ and the inclusion of $R$.

Mathlib.LinearAlgebra.GeneralLinearGroup.Basic

LinearMap.GeneralLinearGroupdefMathlib.LinearAlgebra.GeneralLinearGroup.Basic, type

Wording

general linear group of R and M (from the name)

English

Let $R$ and $M$ be sets. Then a general linear group of $R$ and $M$ is an element of the function that maps $R$ and $M$ to the set of units of the set of linear maps of $M$ and $M$.

LinearMap.GeneralLinearGroup.congrLinearEquivdefMathlib.LinearAlgebra.GeneralLinearGroup.Basic, function or constant

Wording

the congruence linear equivalence of x12 (from the name)

English

Let $x_{12}$ be a linear equivalence of $x_{2}$ and $x_{3}$. Then the congruence linear equivalence of $x_{12}$ is a multiplicative equivalence of the set of general linear groups of $x$ and $x_{2}$ and the set of general linear groups of $x_{1}$ and $x_{3}$ defined as the map equivalence of the multiplicative equivalence of the conjugate ring isomorphism of $x_{12}$.

LinearMap.GeneralLinearGroup.generalLinearEquivdefMathlib.LinearAlgebra.GeneralLinearGroup.Basic, function or constant

Wording

the general linear group on R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the general linear group on $R$ and $M$ is a multiplicative equivalence of the set of general linear groups of $R$ and $M$ and the set of linear equivalences of $M$ and $M$.

LinearMap.GeneralLinearGroup.ofLinearEquivdefMathlib.LinearAlgebra.GeneralLinearGroup.Basic, function or constant

Wording

the general linear group of f (from the name)

English

Let $f$ be a linear equivalence of $M$ and $M$. Then the general linear group of $f$ is a general linear group of $R$ and $M$.

LinearMap.GeneralLinearGroup.toLinearEquivdefMathlib.LinearAlgebra.GeneralLinearGroup.Basic, function or constant

Wording

the linear equivalence of f (from the name)

English

Let $f$ be a general linear group of $R$ and $M$. Then the linear equivalence of $f$ is a linear equivalence of $M$ and $M$.

Mathlib.LinearAlgebra.Goursat

Submodule.goursatFstdefMathlib.LinearAlgebra.Goursat, function or constant

Wording

no wording

English

Let $L$ be a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$. Then $\operatorname{goursatFst}$ applied to $L$ is a submodule of $R$ and $M$ defined as the map of the composition of the first component of $M$ and $N$ and the subtype of $L$ and the kernel of the composition of the second component of $M$ and $N$ and the subtype of $L$.

Submodule.goursatSnddefMathlib.LinearAlgebra.Goursat, function or constant

Wording

no wording

English

Let $L$ be a submodule of $R$ and $\mathrm{Prod}$ applied to $M$ and $N$. Then $\operatorname{goursatSnd}$ applied to $L$ is a submodule of $R$ and $N$ defined as the map of the composition of the second component of $M$ and $N$ and the subtype of $L$ and the kernel of the composition of the first component of $M$ and $N$ and the subtype of $L$.

Mathlib.LinearAlgebra.InvariantBasisNumber

InvariantBasisNumberclassMathlib.LinearAlgebra.InvariantBasisNumber, predicate

Wording

R is a invariant basis number (from the name)

English

Let $R$ be a set. Then we can say that $R$ is an invariant basis number.

RankConditionclassMathlib.LinearAlgebra.InvariantBasisNumber, predicate

Wording

R is a rank condition (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a rank condition.

StrongRankConditionclassMathlib.LinearAlgebra.InvariantBasisNumber, predicate

Wording

R is a strong rank condition (from the name)

English

Let $R$ be a set. Then we can say that $R$ is a strong rank condition.

Mathlib.LinearAlgebra.Isomorphisms

LinearMap.liftOfSurjectivedefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the lift of hf (from the name)

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the lift of $\mathrm{hf}$ is an element of $\EquivMACRoAE {(\SubtypeSet {g}{\mathrm{Leq} (\operatorname{ker} (f), \operatorname{ker} (g))})}{\mathrm{LinearMap} (x , x_{1})}$.

LinearMap.quotKerEquivOfSurjectivedefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient kernel equivalence of f and hf (from the name)

English

Let $f$ be a linear map of $M$ and $x$ such that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then the quotient kernel equivalence of $f$ and $\mathrm{hf}$ is a linear equivalence of the set of quotients of $M$ and the kernel of $f$ and $x$.

LinearMap.quotKerEquivRangedefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient kernel equivalence range of f (from the name)

English

Let $f$ be a linear map of $M$ and $x$. Then the quotient kernel equivalence range of $f$ is a linear equivalence of the set of quotients of $M$ and the kernel of $f$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{6}})}$.

LinearMap.quotientInfEquivSupQuotientdefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient infimum equivalence supremum quotient of p and #2 (from the name)

English

Let $p$ and $\mathrm{p'}$ be submodules of $R$ and $M$. Then the quotient infimum equivalence supremum quotient of $p$ and $\mathrm{p'}$ is a linear equivalence of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and the minimum of the preimage of the subtype of $p$ and $p$ and the preimage of the subtype of $p$ and $\mathrm{p'}$ and the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {p}{\mathrm{p'}})}{x_{4}})}$ and the preimage of the subtype of $\MaxmaxMACRoAF {p}{\mathrm{p'}}$ and $\mathrm{p'}$.

LinearMap.quotientInfToSupQuotientdefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient infimum to supremum quotient of p and #2 (from the name)

English

Let $p$ and $\mathrm{p'}$ be submodules of $R$ and $M$. Then the quotient infimum to supremum quotient of $p$ and $\mathrm{p'}$ is a linear map of the set of quotients of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and the minimum of the preimage of the subtype of $p$ and $p$ and the preimage of the subtype of $p$ and $\mathrm{p'}$ and the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {p}{\mathrm{p'}})}{x_{4}})}$ and the preimage of the subtype of $\MaxmaxMACRoAF {p}{\mathrm{p'}}$ and $\mathrm{p'}$ defined as the lift of the preimage of the subtype of $p$ and $\MinminMACRoAG {p}{\mathrm{p'}}$ and the difference to supremum quotient of $p$ and $\mathrm{p'}$.

LinearMap.subToSupQuotientdefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the difference to supremum quotient of p and #2 (from the name)

English

Let $p$ and $\mathrm{p'}$ be submodules of $R$ and $M$. Then the difference to supremum quotient of $p$ and $\mathrm{p'}$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and the set of quotients of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {(\MaxmaxMACRoAF {p}{\mathrm{p'}})}{x_{4}})}$ and the preimage of the subtype of $\MaxmaxMACRoAF {p}{\mathrm{p'}}$ and $\mathrm{p'}$.

Submodule.quotientQuotientEquivQuotientdefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient quotient equivalence quotient of S and T (from the name)

English

Let $S$ and $T$ be submodules of $R$ and $M$ such that $S \leq T$. Then the quotient quotient equivalence quotient of $S$ and $T$ is a linear equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mkQ}$ applied to $S$ and $T$ and the set of quotients of $M$ and $T$.

Submodule.quotientQuotientEquivQuotientSupdefMathlib.LinearAlgebra.Isomorphisms, function or constant

Wording

the quotient quotient equivalence quotient supremum of S and T (from the name)

English

Let $S$ and $T$ be submodules of $R$ and $M$. Then the quotient quotient equivalence quotient supremum of $S$ and $T$ is a linear equivalence of the set of quotients of the set of quotients of $M$ and $S$ and the map of $\operatorname{mkQ}$ applied to $S$ and $T$ and the set of quotients of $M$ and $\MaxmaxMACRoAF {S}{T}$.

Mathlib.LinearAlgebra.Lagrange

Lagrange.basisdefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

the basis of v and i (from the name)

English

Let $s$ be a finite set of $x_{1}$. Let $v$ be a function from elements of $x_{1}$ to elements of $F$. Let $i$ be an element of $x_{1}$. Then the basis of $v$ and $i$ is a polynomial of $F$ defined as $\FinsetProd {\operatorname{erase} (s , i)}{j}{\operatorname{basisDivisor} (v (i), v (j))}$.

Lagrange.basisDivisordefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

the basis divisor of x1 and y (from the name)

English

Let $x_{1}$ and $y$ be elements of $F$. Then the basis divisor of $x_{1}$ and $y$ is a polynomial of $F$ defined as $\operatorname{C} (\operatorname{inv} (x_{1} - y))\times (\operatorname{X} - \operatorname{C} (y))$.

Lagrange.funEquivDegreeLTdefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

no wording

English

Assume that $v$ is injective on $s$. Then $\operatorname{funEquivDegreeLT}$ applied to $\mathrm{hvs}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{degreeLT} (F , \FinsetcardMACRoM {s})}{x_{3}})}$ and the set of functions from elements of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {s}{x_{5}})}$ to elements of $F$.

Lagrange.interpolatedefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x_{1}$. Let $v$ be a function from elements of $x_{1}$ to elements of $F$. Then $\operatorname{interpolate}$ applied to $s$ and $v$ is a linear map of the set of functions from elements of $x_{1}$ to elements of $F$ and the set of polynomials of $F$.

Lagrange.nodaldefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x_{1}$. Let $v$ be a function from elements of $x_{1}$ to elements of $R$. Then $\operatorname{nodal}$ applied to $s$ and $v$ is a polynomial of $R$ defined as $\FinsetProd {s}{i}{(\operatorname{X} - \operatorname{C} (v (i)))}$.

Lagrange.nodalWeightdefMathlib.LinearAlgebra.Lagrange, function or constant

Wording

no wording

English

Let $s$ be a finite set of $x_{1}$. Let $v$ be a function from elements of $x_{1}$ to elements of $F$. Let $i$ be an element of $x_{1}$. Then $\operatorname{nodalWeight}$ applied to $s$, $v$ and $i$ is an element of $F$ defined as $\FinsetProd {\operatorname{erase} (s , i)}{j}{\operatorname{inv} (v (i)- v (j))}$.

Mathlib.LinearAlgebra.LinearDisjoint

Submodule.LinearDisjointstructureMathlib.LinearAlgebra.LinearDisjoint, predicate

Wording

no wording

English

Let $M$ and $N$ be submodules of $R$ and $S$. Then we can say that $\operatorname{LinearDisjoint}$ holds for $M$ and $N$.

Submodule.LinearDisjoint.mulMapdefMathlib.LinearAlgebra.LinearDisjoint, function or constant

Wording

the multiplicative map of H (from the name)

English

Assume that $\operatorname{LinearDisjoint}$ holds for $M$ and $N$. Then the multiplicative map of $H$ is a linear equivalence of the set of tensor products of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {M}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {N}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {(M \times N)}{x_{5}})}$ defined as the composition of the linear equivalence of the multiplicative map of $M$ and $N$ and $\operatorname{injective}$ applied to $H$ and the linear equivalence of the range of the multiplicative map of $M$ and $N$ and $M \times N$.

Mathlib.LinearAlgebra.LinearIndependent.Defs

LinearIndepOndefMathlib.LinearAlgebra.LinearIndependent.Defs, predicate

Wording

no wording

English

Let $R$ be a set. Let $v$ be a function from elements of $x$ to elements of $M$. Let $s$ be an element of $\wp x$. Then $\mathrm{LinearIndepOn}$ holds for $R$, $v$ and $s$, if $\mathrm{LinearIndependent}$ holds for $R$ and the function that maps $x_{4}$ to $v$ applied to $x_{4}$.

LinearIndependentdefMathlib.LinearAlgebra.LinearIndependent.Defs, predicate

Wording

no wording

English

Let $R$ be a set. Let $v$ be a function from elements of $x$ to elements of $M$. Then $\mathrm{LinearIndependent}$ holds for $R$ and $v$, if $\operatorname{coe}$ applied to the linear combination of $R$ and $v$ is injective.

LinearIndependent.MaximaldefMathlib.LinearAlgebra.LinearIndependent.Defs, predicate

Wording

_i is maximal (from the docstring)

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $v$. Then $\mathrm{\_i}$ is maximal, if for all elements $s$ of $\wp M$, if $\mathrm{LinearIndependent}$ holds for $R$ and the function that maps $x_{4}$ to $\MembershipmemMACRoT {s}{x_{4}}$, then if the range of $v$ is less than or equal to $s$, then the range of $v$ is equal to $s$.

LinearIndependent.linearCombinationEquivdefMathlib.LinearAlgebra.LinearIndependent.Defs, function or constant

Wording

the linear combination equivalence of hv (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $v$. Then the linear combination equivalence of $\mathrm{hv}$ is a linear equivalence of $\FinsuppMACRoQ {x}{R}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{range} (v))}{x_{4}})}$.

LinearIndependent.reprdefMathlib.LinearAlgebra.LinearIndependent.Defs, function or constant

Wording

the representation of hv (from the name)

English

Assume that $\mathrm{LinearIndependent}$ holds for $R$ and $v$. Then the representation of $\mathrm{hv}$ is a linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{range} (v))}{x_{4}})}$ and $\FinsuppMACRoQ {x}{R}$ defined as $\operatorname{toLinearMap}$ applied to the inverse of the linear combination equivalence of $\mathrm{hv}$.

Mathlib.LinearAlgebra.LinearIndependent.Lemmas

LinearIndepOn.extenddefMathlib.LinearAlgebra.LinearIndependent.Lemmas, function or constant

Wording

no wording

English

Assume that $\mathrm{LinearIndepOn}$ holds for $K$, $v$ and $s$. Assume that $s \leq t$. Then $\operatorname{extend}$ applied to $\mathrm{hs}$ and $\mathrm{hst}$ is an element of $\wp x$ defined as $\operatorname{choose}$ applied to $\mathrm{exists\_linearIndepOn\_extension}$ applied to $\mathrm{hs}$ and $\mathrm{hst}$.

equiv_linearIndependentdefMathlib.LinearAlgebra.LinearIndependent.Lemmas, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{equiv\_linearIndependent}$ applied to $n$ is an equivalence from $\SubtypeSet {s}{\mathrm{LinearIndependent} (K , s)}$ to $\Sigma$ applied to the function that maps $s_{1}$ to the set of elements of the complement of the span of $K$ and the range of $s_{1}$.

Mathlib.LinearAlgebra.LinearPMap

LinearMap.compPMapdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

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

English

Let $g$ be a linear map of $F$ and $G$. Let $f$ be a linear map of $E$ and $F$. Then the composition map of $g$ and $f$ is a linear map of $E$ and $G$ defined as $\operatorname{mk}$ applied to the domain of $f$ and the composition of $g$ and the linear map of $f$.

LinearMap.toPMapdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the map of f and p (from the name)

English

Let $f$ be a linear map of $E$ and $F$. Let $p$ be a submodule of $R$ and $E$. Then the map of $f$ and $p$ is a linear map of $E$ and $F$ defined as $\operatorname{mk}$ applied to $p$ and the composition of $f$ and the subtype of $p$.

LinearPMapstructureMathlib.LinearAlgebra.LinearPMap, type

Wording

linear map of E and F (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $E$ and $F$ be sets. Then the linear maps of $E$ and $F$ are a basic type.

LinearPMap.codRestrictdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $E$ and $F$. Let $p$ be a submodule of $S$ and $F$ such that for all elements $x_{8}$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{9}})}$, $\MembershipmemMACRoT {p}{\operatorname{toFun'} (f , x_{8})}$. Then $\operatorname{codRestrict}$ applied to $f$, $p$ and $H$ is a linear map of $E$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {p}{x_{7}})}$ defined as $\operatorname{mk}$ applied to the domain of $f$ and $\operatorname{codRestrict}$ applied to $p$, the linear map of $f$ and $H$.

LinearPMap.compdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the composition of g and f (from the name)

English

Let $g$ be a linear map of $F$ and $G$. Let $f$ be a linear map of $E$ and $F$ such that for all elements $x_{12}$ of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{13}})}$, $\MembershipmemMACRoT {\operatorname{domain} (g)}{\operatorname{toFun'} (f , x_{12})}$. Then the composition of $g$ and $f$ is a linear map of $E$ and $G$ defined as the composition map of the linear map of $g$ and $\operatorname{codRestrict}$ applied to $f$, the domain of $g$ and $H$.

LinearPMap.coproddefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the coproduct of f and g (from the name)

English

Let $f$ be a linear map of $E$ and $G$. Let $g$ be a linear map of $F$ and $G$. Then the coproduct of $f$ and $g$ is a linear map of $\mathrm{Prod}$ applied to $E$ and $F$ and $G$.

LinearPMap.domRestrictdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $E$ and $F$. Let $S_{1}$ be a submodule of $R$ and $E$. Then $\operatorname{domRestrict}$ applied to $f$ and $S_{1}$ is a linear map of $E$ and $F$.

LinearPMap.domaindefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the domain of self (from the name)

English

Let $\mathrm{self}$ be a linear map of $E$ and $F$. Then the domain of $\mathrm{self}$ is a submodule of $R$ and $E$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

LinearPMap.eqLocusdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

no wording

English

Let $f$ and $g$ be linear maps of $E$ and $F$. Then $\operatorname{eqLocus}$ applied to $f$ and $g$ is a submodule of $R$ and $E$.

LinearPMap.fstdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the first component of p and #2 (from the name)

English

Let $p$ be a submodule of $R$ and $E$. Let $\mathrm{p'}$ be a submodule of $R$ and $F$. Then the first component of $p$ and $\mathrm{p'}$ is a linear map of $\mathrm{Prod}$ applied to $E$ and $F$ and $E$ defined as $\operatorname{mk}$ applied to the product of $p$ and $\mathrm{p'}$ and the composition of the first component of $E$ and $F$ and the subtype of the product of $p$ and $\mathrm{p'}$.

LinearPMap.graphdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the graph of f (from the docstring)

English

Let $f$ be a linear map of $E$ and $F$. Then the graph of $f$ is a submodule of $R$ and $\mathrm{Prod}$ applied to $E$ and $F$ defined as the map of the product map of the subtype of the domain of $f$ and the identity and the graph of the linear map of $f$.

LinearPMap.inversedefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the inverse of f (from the docstring)

English

Let $f$ be a linear map of $E$ and $F$. Then the inverse of $f$ is a linear map of $F$ and $E$ defined as the linear map of the map of $\operatorname{toLinearMap}$ applied to $\operatorname{prodComm}$ applied to $R$, $E$ and $F$ and the graph of $f$.

LinearPMap.kerdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a linear map of $E$ and $F$. Then the kernel of $f$ is a submodule of $R$ and $E$ defined as the map of the subtype of the domain of $f$ and the kernel of the linear map of $f$.

LinearPMap.mkSpanSingletondefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the span singleton of x7 and y (from the name)

English

Let $x_{7}$ be an element of $E$. Let $y$ be an element of $F$. Assume that $x_{7} \neq 0$. Then the span singleton of $x_{7}$ and $y$ is a linear map of $E$ and $F$.

LinearPMap.mkSpanSingleton'defMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the span singleton of x7 and y (from the name)

English

Let $x_{7}$ be an element of $E$. Let $y$ be an element of $F$ such that for all elements $c$ of $R$, if $\EqtMACRoH {\HSMulhSMulMACRoAL {c}{x_{7}}}{0}$, then $\EqtMACRoH {\HSMulhSMulMACRoAL {x_{2} (c)}{y}}{0}$. Then the span singleton of $x_{7}$ and $y$ is a linear map of $E$ and $F$.

LinearPMap.sSupdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the supremum of c and hc (from the name)

English

Let $c$ be an element of the power set of the set of linear maps of $E$ and $F$ such that $\mathrm{DirectedOn}$ holds for the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Leq} (x_{7} , x_{8})$ and $c$. Then the supremum of $c$ and $\mathrm{hc}$ is a linear map of $E$ and $F$.

LinearPMap.snddefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the second component of p and #2 (from the name)

English

Let $p$ be a submodule of $R$ and $E$. Let $\mathrm{p'}$ be a submodule of $R$ and $F$. Then the second component of $p$ and $\mathrm{p'}$ is a linear map of $\mathrm{Prod}$ applied to $E$ and $F$ and $F$ defined as $\operatorname{mk}$ applied to the product of $p$ and $\mathrm{p'}$ and the composition of the second component of $E$ and $F$ and the subtype of the product of $p$ and $\mathrm{p'}$.

LinearPMap.supdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the supremum of f and g (from the name)

English

Let $f$ and $g$ be linear maps of $E$ and $F$ such that for all elements $x_{7}$ of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{9}})}$, for all elements $y$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{domain} (g)}{x_{8}})}$, if $\EqtMACRoH {x_{7}}{y}$, then $\EqtMACRoH {\operatorname{toFun'} (f , x_{7})}{\operatorname{toFun'} (g , y)}$. Then the supremum of $f$ and $g$ is a linear map of $E$ and $F$.

LinearPMap.supSpanSingletondefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the supremum span singleton of x7 and y (from the name)

English

Let $f$ be a linear map of $E$ and $F$. Let $x_{7}$ be an element of $E$. Let $y$ be an element of $F$. Assume that $x_{7}$ is not an element of the domain of $f$. Then the supremum span singleton of $x_{7}$ and $y$ is a linear map of $E$ and $F$.

LinearPMap.toFundefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the linear map of self (from the name)

English

Let $\mathrm{self}$ be a linear map of $E$ and $F$. Then the linear map of $\mathrm{self}$ is a linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{domain} (\mathrm{self})}{x_{7}})}$ and $F$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

LinearPMap.toFun'defMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the function of f and x7 (from the name)

English

Let $f$ be a linear map of $E$ and $F$. Let $x_{7}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{domain} (f)}{x_{8}})}$. Then the function of $f$ and $x_{7}$ is an element of $F$ defined as the coercion of the linear map of $f$ and $x_{7}$.

Submodule.toLinearPMapdefMathlib.LinearAlgebra.LinearPMap, function or constant

Wording

the linear map of g (from the name)

English

Let $g$ be a submodule of $R$ and $\mathrm{Prod}$ applied to $E$ and $F$. Then the linear map of $g$ is a linear map of $E$ and $F$ defined as $\operatorname{mk}$ applied to the map of the first component of $E$ and $F$ and $g$ and $\mathrm{dite}$ applied to the proposition that for all elements $x_{5}$ of $\mathrm{Prod}$ applied to $E$ and $F$, if $x_{5}$ is an element of $g$, then if $\EqtMACRoH {\ProdfstMACRoZ {x_{5}}}{0}$, then $\EqtMACRoH {\ProdsndMACRoAA {x_{5}}}{0}$, the function that maps $\mathrm{hg}$ to $\operatorname{toLinearPMapAux}$ applied to $g$ and $\mathrm{hg}$ and the function that maps $\mathrm{hg1}$ to $0$.

Mathlib.LinearAlgebra.Matrix.Adjugate

Matrix.adjugatedefMathlib.LinearAlgebra.Matrix.Adjugate, function or constant

Wording

the adjugate matrix of A (from the docstring)

English

Let $A$ be a matrix of $n$ and $x$. Then the adjugate matrix of $A$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ to $\operatorname{cramer}$ applied to the transpose of $A$ and $\operatorname{single}$ applied to $i_{1}$ and $1$.

Matrix.cramerdefMathlib.LinearAlgebra.Matrix.Adjugate, function or constant

Wording

the cramer of A (from the name)

English

Let $A$ be a matrix of $n$ and $x$. Then the cramer of $A$ is a linear map of the set of functions from elements of $n$ to elements of $x$ and the set of functions from elements of $n$ to elements of $x$ defined as $\operatorname{mk'}$ applied to $\operatorname{cramerMap}$ and $\mathrm{Matrix\_\_cramer\_is\_linear}$ applied to $A$.

Matrix.cramerMapdefMathlib.LinearAlgebra.Matrix.Adjugate, function or constant

Wording

the cramer map of b and i (from the name)

English

Let $A$ be a matrix of $n$ and $x$. Let $b$ be a function from elements of $n$ to elements of $x$. Let $i$ be an element of $n$. Then the cramer map of $b$ and $i$ is an element of $x$ defined as the determinant of $\operatorname{updateCol}$ applied to $A$, $i$ and $b$.

Mathlib.LinearAlgebra.Matrix.Array

Matrix.ofArraydefMathlib.LinearAlgebra.Matrix.Array, function or constant

Wording

the matrix of A and hA (from the name)

English

Let $A$ be an element of $\mathrm{Array}$ applied to $R$ such that $\operatorname{size} (A)= m \times n$. Then the matrix of $A$ and $\mathrm{hA}$ is a matrix of $\mathrm{Fin}$ applied to $n$ and $R$.

Matrix.toArraydefMathlib.LinearAlgebra.Matrix.Array, function or constant

Wording

the array of the entries of A (from the docstring)

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $R$. Then the array of the entries of $A$ is an element of $\mathrm{Array}$ applied to $R$ defined as $\operatorname{ofFn}$ applied to the function that maps $k$ to $A$ applied to $\operatorname{divNat}$ applied to $k$ and $\operatorname{modNat}$ applied to $k$.

Mathlib.LinearAlgebra.Matrix.Basis

Module.Basis.toMatrixdefMathlib.LinearAlgebra.Matrix.Basis, function or constant

Wording

the matrix of e and v (from the name)

English

Let $e$ be a basis of $R$ and $M$. Let $v$ be a function from elements of $x_{1}$ to elements of $M$. Then the matrix of $e$ and $v$ is a matrix of $x_{1}$ and $R$ defined as the function that maps $i$ and $j$ to $\operatorname{coe}$ applied to the representation of $e$, $v$ applied to $j$ and $i$.

Module.Basis.toMatrixEquivdefMathlib.LinearAlgebra.Matrix.Basis, function or constant

Wording

the matrix equivalence of e (from the name)

English

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

Mathlib.LinearAlgebra.Matrix.Bilinear

mulLeftLinearMapdefMathlib.LinearAlgebra.Matrix.Bilinear, function or constant

Wording

the multiplicative left linear map of X (from the name)

English

Let $n$ and $R$ be sets. Let $X$ be a matrix of $m$ and $A$. Then the multiplicative left linear map of $X$ is a linear map of the set of matrixes of $n$ and $A$ and the set of matrixes of $n$ and $A$.

mulLinearMapdefMathlib.LinearAlgebra.Matrix.Bilinear, function or constant

Wording

the multiplicative linear map of R (from the name)

English

Let $R$ be a set. Then the multiplicative linear map of $R$ is a linear map of the set of matrixes of $m$ and $A$ and the set of linear maps of the set of matrixes of $n$ and $A$ and the set of matrixes of $n$ and $A$.

mulRightLinearMapdefMathlib.LinearAlgebra.Matrix.Bilinear, function or constant

Wording

the multiplicative right linear map of Y (from the name)

English

Let $l$ and $R$ be sets. Let $Y$ be a matrix of $n$ and $A$. Then the multiplicative right linear map of $Y$ is a linear map of the set of matrixes of $m$ and $A$ and the set of matrixes of $n$ and $A$.

Mathlib.LinearAlgebra.Matrix.BilinearForm

LinearMap.BilinForm.toMatrixdefMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the matrix of b (from the name)

English

Let $b$ be a basis of $x$ and $x_{1}$. Then the matrix of $b$ is a linear equivalence of the set of bilinear forms of $x$ and $x_{1}$ and the set of matrixes of $n$ and $x$ defined as the matrix of $b$ and $b$.

LinearMap.BilinForm.toMatrix'defMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the matrix (from the name)

English

The matrix is a linear equivalence of the set of bilinear forms of $x$ and the set of functions from elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$ defined as the matrix of $x$.

Matrix.toBilindefMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the bilinear of b (from the name)

English

Let $b$ be a basis of $x$ and $x_{1}$. Then the bilinear of $b$ is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of bilinear forms of $x$ and $x_{1}$ defined as the inverse of the matrix of $b$.

Matrix.toBilin'defMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the bilinear (from the name)

English

The bilinear is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of bilinear forms of $x$ and the set of functions from elements of $n$ to elements of $x$ defined as the inverse of the matrix.

selfAdjointMatricesSubmodule'defMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the self adjoint matrice submodule of J (from the name)

English

Let $J$ be a matrix of $n$ and $x$. Then the self adjoint matrice submodule of $J$ is a submodule of $x$ and the set of matrixes of $n$ and $x$ defined as the pair self adjoint matrice submodule of $J$ and $J$.

skewAdjointMatricesSubmodule'defMathlib.LinearAlgebra.Matrix.BilinearForm, function or constant

Wording

the skew adjoint matrice submodule of J (from the name)

English

Let $J$ be a matrix of $n$ and $x$. Then the skew adjoint matrice submodule of $J$ is a submodule of $x$ and the set of matrixes of $n$ and $x$ defined as the pair self adjoint matrice submodule of $\operatorname{neg}$ applied to $J$ and $J$.

Mathlib.LinearAlgebra.Matrix.Block

Matrix.BlockTriangulardefMathlib.LinearAlgebra.Matrix.Block, predicate

Wording

no wording

English

Let $M$ be a matrix of $m$ and $R$. Let $b$ be a function from elements of $m$ to elements of $x$. Then $\operatorname{BlockTriangular}$ holds for $M$ and $b$, if for all elements $i$ and $j$ of $m$, if $b (j)< b (i)$, then $\EqtMACRoH {M (i , j)}{0}$.

Matrix.IsIndecomposabledefMathlib.LinearAlgebra.Matrix.Block, predicate

Wording

M is indecomposable (from the docstring)

English

Let $M$ be a matrix of $m$ and $R$. Then $M$ is indecomposable, if for all natural numbers $i$ and $j$, for all matrixes $A$ of $\mathrm{Fin}$ applied to $i$ and $R$, for all matrixes $B$ and $D$ of $\mathrm{Fin}$ applied to $j$ and $R$, for all elements $e$ of $\EquivMACRoAE {\mathrm{Sum} (\mathrm{Fin} (i), \mathrm{Fin} (j))}{m}$, if $\EqtMACRoH {M}{\operatorname{reindex} (e , e , \operatorname{fromBlocks} (A , B , 0 , D))}$, then $i = 0$ or $j = 0$.

Matrix.IsLowerTriangulardefMathlib.LinearAlgebra.Matrix.Block, predicate

Wording

no wording

English

Let $M$ be a matrix of $m$ and $R$. Then $\operatorname{IsLowerTriangular}$ holds for $M$, if $\operatorname{BlockTriangular}$ holds for $M$ and $\operatorname{coe}$ applied to the dual.

Matrix.IsUpperTriangulardefMathlib.LinearAlgebra.Matrix.Block, predicate

Wording

no wording

English

Let $M$ be a matrix of $m$ and $R$. Then $\operatorname{IsUpperTriangular}$ holds for $M$, if $\operatorname{BlockTriangular}$ holds for $M$ and $\mathrm{id}$.

Matrix.blockTriangularSubalgebradefMathlib.LinearAlgebra.Matrix.Block, function or constant

Wording

the block triangular subalgebra of b (from the name)

English

Let $R$ and $A$ be sets. Let $b$ be a function from elements of $m$ to elements of $x$. Then the block triangular subalgebra of $b$ is a subalgebra of $R$ and the set of matrixes of $m$ and $A$ defined as $\operatorname{mk}$ applied to the block triangular subsemiring of $A$ and $b$ and the function that maps $r$ to $\mathrm{Matrix\_\_blockTriangular\_algebraMap}$ applied to $r$.

Matrix.blockTriangularSubsemiringdefMathlib.LinearAlgebra.Matrix.Block, function or constant

Wording

the block triangular subsemiring of R and b (from the name)

English

Let $R$ be a set. Let $b$ be a function from elements of $m$ to elements of $x$. Then the block triangular subsemiring of $R$ and $b$ is a subsemiring of the set of matrixes of $m$ and $R$.

Mathlib.LinearAlgebra.Matrix.Cartan.Basic

CartanMatrix.AdefMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

CartanMatrix.BdefMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

CartanMatrix.CdefMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

CartanMatrix.DdefMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $\Integer$. Proof. Let $n$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By Eqt. By 2. By n. By 2. By Leq. By 0. By i1. By Fin__val. By 1. By plus. By j1. By Fin__val. By Eq. By j1. By Fin__val. By 2. By plus. By n. By Lt. By and. By 1. By Neg__neg. By j1. By Fin__val. By 1. By plus. By i1. By Fin__val. By Eq. By i1. By Fin__val. By 2. By plus. By n. By Lt. By and. By 1. By Neg__neg. By i1. By Fin__val. By 3. By plus. By n. By Eq. By j1. By Fin__val. By 2. By plus. By n. By Eq. By j1. By Fin__val. By 1. By plus. By n. By Eq. By or. By and. By 1. By Neg__neg. By j1. By Fin__val. By 3. By plus. By n. By Eq. By i1. By Fin__val. By 2. By plus. By n. By Eq. By i1. By Fin__val. By 1. By plus. By n. By Eq. By or. By and. By 1. By Neg__neg. By 0. By ite. By ite. By ite. By ite. By ite. By ite. By Matrix__of__app.

CartanMatrix.EdefMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $\Integer$. Proof. Let $n$ be arbitrary. Let $i_{1}$ be arbitrary. Let $j_{1}$ be arbitrary. By i1. By j1. By Eqt. By 2. By i1. By Fin__val. By 0. By Eq. By j1. By Fin__val. By 2. By Eq. By and. By j1. By Fin__val. By 0. By Eq. By i1. By Fin__val. By 2. By Eq. By and. By i1. By Fin__val. By 1. By Eq. By j1. By Fin__val. By 3. By Eq. By and. By j1. By Fin__val. By 1. By Eq. By i1. By Fin__val. By 3. By Eq. By and. By 2. By i1. By Fin__val. By Leq. By i1. By Fin__val. By 1. By plus. By j1. By Fin__val. By Eq. By and. By 2. By j1. By Fin__val. By Leq. By j1. By Fin__val. By 1. By plus. By i1. By Fin__val. By Eq. By and. By or. By or. By or. By or. By or. By 1. By Neg__neg. By 0. By ite. By ite. By Matrix__of__app.

CartanMatrix.F₄defMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

There is a matrix of $\mathrm{Fin}$ applied to $4$ and $\Integer$. Proof. By 2. By 1. By Neg__neg. By 0. By 0. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By 1. By Neg__neg. By 2. By 2. By Neg__neg. By 0. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By 0. By 1. By Neg__neg. By 2. By 1. By Neg__neg. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By 0. By 0. By 1. By Neg__neg. By 2. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecCons. By Matrix__of__app.

CartanMatrix.G₂defMathlib.LinearAlgebra.Matrix.Cartan.Basic, function or constant

Wording

no wording

English

There is a matrix of $\mathrm{Fin}$ applied to $2$ and $\Integer$. Proof. By 2. By 3. By Neg__neg. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By 1. By Neg__neg. By 2. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__vecEmpty. By Matrix__vecCons. By Matrix__vecCons. By Matrix__of__app.

Matrix.IsFiniteCartanstructureMathlib.LinearAlgebra.Matrix.Cartan.Basic, predicate

Wording

no wording

English

Let $M$ be a matrix of $x$ and $\Integer$. Then we can say that $\operatorname{IsFiniteCartan}$ holds for $M$.

Matrix.IsSimplyLaceddefMathlib.LinearAlgebra.Matrix.Cartan.Basic, predicate

Wording

no wording

English

Let $A$ be a matrix of $x$ and $\Integer$. Then $\operatorname{IsSimplyLaced}$ holds for $A$, if the function that maps $i$ and $j$ to the proposition that $A (i , j)= 0$ or $A (i , j)= \operatorname{neg} (1)$ is pairwise.

Mathlib.LinearAlgebra.Matrix.Cartan.Realisation

CartanMatrix.RealisationstructureMathlib.LinearAlgebra.Matrix.Cartan.Realisation, type

Wording

realisation of M and N (from the name)

English

Let $n$, $R$, $M$ and $N$ be sets. Then the realisations of $M$ and $N$ are a basic type.

CartanMatrix.Realisation.baseIdxdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the base index of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the base index of $\mathrm{rl}$ is an embedding of $n$ and the set of elements of the index of $\mathrm{rl}$.

CartanMatrix.Realisation.coreflectiondefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

no wording

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Let $i$ be an element of $n$. Then $\operatorname{coreflection}$ applied to $\mathrm{rl}$ and $i$ is a linear equivalence of $N$ and $N$ defined as the reflection of the flip of $\mathrm{rl}$ and $i$.

CartanMatrix.Realisation.flipdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the flip of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the flip of $\mathrm{rl}$ is a realisation of $N$ and $M$.

CartanMatrix.Realisation.idxdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the index of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the index of $\mathrm{rl}$ is an element of $\wp \mathrm{Prod} (M , N)$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{7}$ to the proposition that there exists an element $w$ of $\mathrm{Prod}$ applied to the set of linear equivalences of $M$ and $M$ and the set of linear equivalences of $N$ and $N$, such that $\MembershipmemMACRoT {\operatorname{weylGroup} (\mathrm{rl})}{w}$ and there exists an element $i$ of $n$ such that $\EqtMACRoH {\ProdmkMACRoU {\operatorname{fst} (w , \operatorname{sRoot} (\mathrm{rl} , i))}{\operatorname{snd} (w , \operatorname{sCoroot} (\mathrm{rl} , i))}}{x_{7}}$.

CartanMatrix.Realisation.matrixdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the Cartan matrix of self (from the docstring)

English

Let $\mathrm{self}$ be a realisation of $M$ and $N$. Then the Cartan matrix of $\mathrm{self}$ is a matrix of $n$ and $\Integer$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$.

CartanMatrix.Realisation.pairingdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the perfect pairing of self (from the docstring)

English

Let $\mathrm{self}$ be a realisation of $M$ and $N$. Then the perfect pairing of $\mathrm{self}$ is a linear map of $M$ and the set of linear maps of $N$ and $R$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

CartanMatrix.Realisation.reflectiondefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the reflection of rl and i (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Let $i$ be an element of $n$. Then the reflection of $\mathrm{rl}$ and $i$ is a linear equivalence of $M$ and $M$.

CartanMatrix.Realisation.reflectionPairdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the reflection pair of rl and hp (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$ such that $p$ is an element of the index of $\mathrm{rl}$. Then the reflection pair of $\mathrm{rl}$ and $\mathrm{hp}$ is an element of $\mathrm{Prod}$ applied to the set of linear equivalences of $M$ and $M$ and the set of linear equivalences of $N$ and $N$.

CartanMatrix.Realisation.rootPairingBasedefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root pairing base of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the root pairing base of $\mathrm{rl}$ is a base of the root pairing of $\mathrm{rl}$.

CartanMatrix.Realisation.rootPairingBaseEquivdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root pairing base equivalence of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the root pairing base equivalence of $\mathrm{rl}$ is an element of $\EquivMACRoAE {n}{(\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{support} (\operatorname{rootPairingBase} (\mathrm{rl}))}{x_{7}})})}$.

CartanMatrix.Realisation.sCorootdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the coroot of self and x7 (from the name)

English

Let $\mathrm{self}$ be a realisation of $M$ and $N$. Let $x_{7}$ be an element of $n$. Then the coroot of $\mathrm{self}$ and $x_{7}$ is an element of $N$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{7}$.

CartanMatrix.Realisation.sRootdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root of self and x7 (from the name)

English

Let $\mathrm{self}$ be a realisation of $M$ and $N$. Let $x_{7}$ be an element of $n$. Then the root of $\mathrm{self}$ and $x_{7}$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{7}$.

CartanMatrix.Realisation.toRootPairingdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root pairing of rl (from the name)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the root pairing of $\mathrm{rl}$ is a root pairing of $M$ and $N$.

CartanMatrix.Realisation.weylGroupdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the Weyl group of rl (from the docstring)

English

Let $\mathrm{rl}$ be a realisation of $M$ and $N$. Then the Weyl group of $\mathrm{rl}$ is a subgroup of $\mathrm{Prod}$ applied to the set of linear equivalences of $M$ and $M$ and the set of linear equivalences of $N$ and $N$ defined as the closure of the range of $\operatorname{prod}$ applied to $\operatorname{coreflection}$ applied to $\mathrm{rl}$.

Matrix.IsFiniteCartan.rootPairingBasedefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the base of the root system defined by a Cartan matrix of hA and k (from the docstring)

English

Assume that $\operatorname{IsFiniteCartan}$ holds for $A$. Let $k$ be a set. Then the base of the root system defined by a Cartan matrix of $\mathrm{hA}$ and $k$ is a base of the root pairing of $\mathrm{hA}$ and $k$ defined as the root pairing base of the realisation of $\mathrm{hA}$ and $\operatorname{invertible}$ applied to $\mathrm{Matrix\_\_IsFiniteCartan\_\_isUnit\_map}$ applied to $\mathrm{hA}$ and $k$.

Matrix.IsFiniteCartan.rootPairingBaseEquivdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root pairing base equivalence of hA and k (from the name)

English

Assume that $\operatorname{IsFiniteCartan}$ holds for $A$. Let $k$ be a set. Then the root pairing base equivalence of $\mathrm{hA}$ and $k$ is an element of $\EquivMACRoAE {n}{(\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{support} (\operatorname{rootPairingBase} (\mathrm{hA} , k))}{x_{3}})})}$ defined as the root pairing base equivalence of the realisation of $\mathrm{hA}$ and $\operatorname{invertible}$ applied to $\mathrm{Matrix\_\_IsFiniteCartan\_\_isUnit\_map}$ applied to $\mathrm{hA}$ and $k$.

Matrix.IsFiniteCartan.toRealisationdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the realisation of hA and hAI (from the name)

English

Assume that $\operatorname{IsFiniteCartan}$ holds for $A$. Assume that the map of $A$ and $\operatorname{toIntCast}$ is invertible. Then the realisation of $\mathrm{hA}$ and $\mathrm{hAI}$ is a realisation of the set of functions from elements of $n$ to elements of $R$ and the set of functions from elements of $n$ to elements of $R$.

Matrix.IsFiniteCartan.toRootPairingdefMathlib.LinearAlgebra.Matrix.Cartan.Realisation, function or constant

Wording

the root pairing of hA and k (from the name)

English

Assume that $\operatorname{IsFiniteCartan}$ holds for $A$. Let $k$ be a set. Then the root pairing of $\mathrm{hA}$ and $k$ is a root pairing of the set of functions from elements of $n$ to elements of $k$ and the set of functions from elements of $n$ to elements of $k$ defined as the root pairing of the realisation of $\mathrm{hA}$ and $\operatorname{invertible}$ applied to $\mathrm{Matrix\_\_IsFiniteCartan\_\_isUnit\_map}$ applied to $\mathrm{hA}$ and $k$.

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Matrix.charmatrixdefMathlib.LinearAlgebra.Matrix.Charpoly.Basic, function or constant

Wording

no wording

English

Let $M$ be a matrix of $n$ and $R$. Then there is a matrix of $n$ and the set of polynomials of $R$. Proof. Let $M$ be arbitrary. By n. By Polynomial__X. By Matrix__scalar__app. By Polynomial__C. By M. By RingHom__mapMatrix__app. By minus.

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

Wording

the characteristic polynomial of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $R$. Then the characteristic polynomial of $M$ is a polynomial of $R$ defined as the determinant of $\operatorname{charmatrix}$ applied to $M$.

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Matrix.charpolyRevdefMathlib.LinearAlgebra.Matrix.Charpoly.Coeff, function or constant

Wording

the reverse of the characteristic polynomial of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $R$. Then the reverse of the characteristic polynomial of $M$ is a polynomial of $R$ defined as the determinant of $1 - \HSMulhSMulMACRoAL {\operatorname{X}}{\operatorname{map} (M , \operatorname{coe} (\operatorname{C}))}$.

Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

Matrix.discrdefMathlib.LinearAlgebra.Matrix.Charpoly.Disc, function or constant

Wording

the discriminant of A (from the docstring)

English

Let $A$ be a matrix of $n$ and $R$. Then the discriminant of $A$ is an element of $R$ defined as the discriminant of the characteristic polynomial of $A$.

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Matrix.RepresentsdefMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap, predicate

Wording

no wording

English

Let $b$ be a function from elements of $x$ to elements of $M$. Let $A$ be a matrix of $x$ and $R$. Let $f$ be an end of $R$ and $M$. Then $\operatorname{Represents}$ holds for $b$, $A$ and $f$, if $\EqtMACRoH {\operatorname{fromMatrix} (R , b , A)}{\operatorname{fromEnd} (R , b , f)}$.

Matrix.isRepresentationdefMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap, function or constant

Wording

no wording

English

Let $R$ be a set. Let $b$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{isRepresentation}$ applied to $R$ and $b$ is a subalgebra of $R$ and the set of matrixes of $x$ and $R$.

Matrix.isRepresentation.toEnddefMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap, function or constant

Wording

the end of b (from the name)

English

Let $R$ be a set. Let $b$ be a function from elements of $x$ to elements of $M$ such that the span of $R$ and the range of $b$ is equal to the top. Then the end of $b$ is an algebra homomorphism of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{isRepresentation} (R , b)}{x_{6}})}$ and the set of ends of $R$ and $M$.

PiToModule.fromEnddefMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap, function or constant

Wording

no wording

English

Let $R$ be a set. Let $b$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{fromEnd}$ applied to $R$ and $b$ is a linear map of the set of ends of $R$ and $M$ and the set of linear maps of the set of functions from elements of $x$ to elements of $R$ and $M$ defined as $\operatorname{lcomp}$ applied to $R$, $M$ and the linear combination of $R$ and $b$.

PiToModule.fromMatrixdefMathlib.LinearAlgebra.Matrix.Charpoly.LinearMap, function or constant

Wording

no wording

English

Let $R$ be a set. Let $b$ be a function from elements of $x$ to elements of $M$. Then $\operatorname{fromMatrix}$ applied to $R$ and $b$ is a linear map of the set of matrixes of $x$ and $R$ and the set of linear maps of the set of functions from elements of $x$ to elements of $R$ and $M$ defined as the composition of $\operatorname{llcomp}$ applied to $R$, the set of functions from elements of $x$ to elements of $R$, the set of functions from elements of $x$ to elements of $R$, $M$ and the linear combination of $R$ and $b$ and the linear map of the inverse of the algebra isomorphism matrix.

Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Matrix.charpoly.univdefMathlib.LinearAlgebra.Matrix.Charpoly.Univ, function or constant

Wording

the universal set of R and n (from the name)

English

Let $R$ and $n$ be sets. Then the universal set of $R$ and $n$ is a polynomial of the set of multivariate polynomials of $\mathrm{Prod}$ applied to $n$ and $n$ and $R$ defined as the characteristic polynomial of the multivariate polynomial of $n$ and $R$.

Mathlib.LinearAlgebra.Matrix.Circulant

Matrix.circulantdefMathlib.LinearAlgebra.Matrix.Circulant, function or constant

Wording

the circulant of v (from the name)

English

Let $v$ be a function from elements of $n$ to elements of $x$. Then the circulant of $v$ is a matrix of $n$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $v$ applied to $i_{1} - j_{1}$.

Mathlib.LinearAlgebra.Matrix.ConjTranspose

Matrix.conjTransposedefMathlib.LinearAlgebra.Matrix.ConjTranspose, function or constant

Wording

the conjugate transpose of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $x$. Then the conjugate transpose of $M$ is a matrix of $m$ and $x$ defined as the map of the transpose of $M$ and $\operatorname{star}$.

Matrix.conjTransposeAddEquivdefMathlib.LinearAlgebra.Matrix.ConjTranspose, function or constant

Wording

the conjugate transpose additive equivalence of n and x (from the name)

English

Let $m$, $n$ and $x$ be sets. Then the conjugate transpose additive equivalence of $n$ and $x$ is an additive equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $m$ and $x$.

Matrix.conjTransposeAlgEquivdefMathlib.LinearAlgebra.Matrix.ConjTranspose, function or constant

Wording

the conjugate transpose algebra isomorphism of n and x (from the name)

English

Let $n$ and $x$ be sets. Then the conjugate transpose algebra isomorphism of $n$ and $x$ is a star algebra isomorphism of the set of matrixes of $n$ and $x$ and the set of multiplicative opposites of the set of matrixes of $n$ and $x$.

Matrix.conjTransposeLinearEquivdefMathlib.LinearAlgebra.Matrix.ConjTranspose, function or constant

Wording

the conjugate transpose linear equivalence of R and x (from the name)

English

Let $m$, $n$, $R$ and $x$ be sets. Then the conjugate transpose linear equivalence of $R$ and $x$ is a linear equivalence of the set of matrixes of $n$ and $x$ and the set of matrixes of $m$ and $x$.

Matrix.conjTransposeRingEquivdefMathlib.LinearAlgebra.Matrix.ConjTranspose, function or constant

Wording

the conjugate transpose ring isomorphism of m and x (from the name)

English

Let $m$ and $x$ be sets. Then the conjugate transpose ring isomorphism of $m$ and $x$ is a star ring isomorphism of the set of matrixes of $m$ and $x$ and the set of multiplicative opposites of the set of matrixes of $m$ and $x$.

Mathlib.LinearAlgebra.Matrix.Defs

MatrixdefMathlib.LinearAlgebra.Matrix.Defs, type

Wording

matrix of n and x (from the name)

English

Let $m$, $n$ and $x$ be sets. Then a matrix of $n$ and $x$ is an element of the function that maps $m$, $n$ and $x$ to the set of functions from elements of $m$ and elements of $n$ to elements of $x$.

Matrix.coldefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $n$ and $x$. Let $x_{1}$ be an element of $n$. Let $x_{2}$ be an element of $m$. Then $\operatorname{col}$ applied to $A$, $x_{1}$ and $x_{2}$ is an element of $x$ defined as the transpose of $A$.

Matrix.mapdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the map of M and f (from the name)

English

Let $M$ be a matrix of $n$ and $x$. Let $f$ be a function from elements of $x$ to elements of $x_{1}$. Then the map of $M$ and $f$ is a matrix of $n$ and $x_{1}$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $f$ applied to $M$ applied to $i_{1}$ and $j_{1}$.

Matrix.ofdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

$\operatorname{of}$ is an equivalence from the set of functions from elements of $m$ and elements of $n$ to elements of $x$ to the set of matrixes of $n$ and $x$ defined as the identity of the set of functions from elements of $m$ and elements of $n$ to elements of $x$.

Matrix.ofAddEquivdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the matrix (from the name)

English

The matrix is an additive equivalence of the set of functions from elements of $m$ and elements of $n$ to elements of $x$ and the set of matrixes of $n$ and $x$.

Matrix.reindexdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the reindexing of x1 and x2 (from the name)

English

Let $x_{1}$ be an equivalence from $m$ to $l$. Let $x_{2}$ be an equivalence from $n$ to $o$. Then the reindexing of $x_{1}$ and $x_{2}$ is an equivalence from the set of matrixes of $n$ and $x$ to the set of matrixes of $o$ and $x$.

Matrix.rowdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the row of x1 and x2 (from the name)

English

Let $A$ be a matrix of $n$ and $x$. Let $x_{1}$ be an element of $m$. Let $x_{2}$ be an element of $n$. Then the row of $x_{1}$ and $x_{2}$ is an element of $x$ defined as $A$ applied to $x_{1}$ and $x_{2}$.

Matrix.subDowndefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Proof. Let $A$ be arbitrary. By u. By Fin__natAdd. By id. By Matrix__submatrix.

Matrix.subDownLeftdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $l + r$ and $x$. Then there is a matrix of $\mathrm{Fin}$ applied to $l$ and $x$. Proof. Let $A$ be arbitrary. By A. By Matrix__subLeft. By Matrix__subDown.

Matrix.subDownRightdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $l + r$ and $x$. Then there is a matrix of $\mathrm{Fin}$ applied to $r$ and $x$. Proof. Let $A$ be arbitrary. By A. By Matrix__subRight. By Matrix__subDown.

Matrix.subLeftdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the left of A (from the docstring)

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $l + r$ and $x$. Then the left of $A$ is a matrix of $\mathrm{Fin}$ applied to $l$ and $x$ defined as the submatrix of $\mathrm{id}$ and $\operatorname{castAdd}$ applied to $r$.

Matrix.subRightdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the right of A (from the docstring)

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $l + r$ and $x$. Then the right of $A$ is a matrix of $\mathrm{Fin}$ applied to $r$ and $x$ defined as the submatrix of $\mathrm{id}$ and $\operatorname{natAdd}$ applied to $l$.

Matrix.subUpdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Then there is a matrix of $\mathrm{Fin}$ applied to $n$ and $x$. Proof. Let $A$ be arbitrary. By d. By Fin__castAdd. By id. By Matrix__submatrix.

Matrix.subUpLeftdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Matrix.subUpRightdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

no wording

English

Matrix.submatrixdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the submatrix of r and c (from the name)

English

Let $A$ be a matrix of $n$ and $x$. Let $r$ be a function from elements of $l$ to elements of $m$. Let $c$ be a function from elements of $o$ to elements of $n$. Then the submatrix of $r$ and $c$ is a matrix of $o$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $A$ applied to $r$ applied to $i_{1}$ and $c$ applied to $j_{1}$.

Matrix.transposedefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the transpose of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $x$. Then the transpose of $M$ is a matrix of $m$ and $x$ defined as $\operatorname{of}$ applied to the function that maps $x_{2}$ and $y_{1}$ to $M$ applied to $y_{1}$ and $x_{2}$.

Set.matrixdefMathlib.LinearAlgebra.Matrix.Defs, function or constant

Wording

the matrix of S (from the name)

English

Let $S$ be an element of $\wp x$. Then the matrix of $S$ is an element of the power set of the set of matrixes of $n$ and $x$ defined as $\operatorname{ofPred}$ applied to the function that maps $M$ to the proposition that for all elements $i$ of $m$, for all elements $j$ of $n$, $\MembershipmemMACRoT {S}{M (i , j)}$.

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Matrix.detdefMathlib.LinearAlgebra.Matrix.Determinant.Basic, function or constant

Wording

the determinant of M (from the docstring)

English

Let $M$ be a matrix of $n$ and $R$. Then the determinant of $M$ is an element of $R$ defined as $\operatorname{detRowAlternating}$ applied to $M$.

Matrix.detMonoidHomdefMathlib.LinearAlgebra.Matrix.Determinant.Basic, function or constant

Wording

the determinant (from the docstring)

English

The determinant is a monoid homomorphism of the set of matrixes of $n$ and $R$ and $R$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{det}$ and $\mathrm{Matrix\_\_det\_one}$ and $\mathrm{Matrix\_\_det\_mul}$.

Matrix.detRowAlternatingdefMathlib.LinearAlgebra.Matrix.Determinant.Basic, function or constant

Wording

no wording

English

$\operatorname{detRowAlternating}$ is an alternating map of $R$ and $n$ defined as $\operatorname{alternatization}$ applied to the composition linear map of the product algebra of $n$ and $R$ and $\operatorname{proj}$.

Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs

BirdDet.Spec.birdDetdefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $\mathrm{Fin}$ applied to $n$ and $R$. Then $\operatorname{birdDet}$ applied to $A$ is an element of $R$.

BirdDet.Spec.stepEntrydefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

the step entry of A and F (from the name)

English

Let $A$ and $F$ be matrixes of $\mathrm{Fin}$ applied to $n$ and $R$. Then the step entry of $A$ and $F$ is a matrix of $\mathrm{Fin}$ applied to $n$ and $R$ defined as $\operatorname{of}$ applied to the function that maps $i_{1}$ and $j_{1}$ to $\operatorname{neg} (\FinsetSum {\operatorname{Ioi} (i_{1})}{k}{F (k , k)})\times A (i_{1} , j_{1})+ \FinsetSum {\operatorname{Ioi} (i_{1})}{k_{1}}{(F (i_{1} , k_{1})\times A (k_{1} , j_{1}))}$.

BirdDet.birdDetdefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $A$ be an element of $\mathrm{Array}$ applied to $R$. Then $\operatorname{birdDet}$ applied to $n$ and $A$ is an element of $R$.

BirdDet.getdefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

no wording

English

Let $n$, $i$ and $j$ be natural numbers. Let $A$ be an element of $\mathrm{Array}$ applied to $R$. Then $\operatorname{get}$ applied to $n$, $A$, $i$ and $j$ is an element of $R$ defined as $\operatorname{getD}$ applied to $A$, $n \times i + j$ and $0$.

BirdDet.stepEntrydefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

the step entry of i and j (from the name)

English

Let $n$, $i$ and $j$ be elements of $\Natural$. Let $A$ be an element of $\mathrm{Array}$ applied to $R$. Let $F$ be a function from natural numbers and natural numbers to elements of $R$. Then the step entry of $i$ and $j$ is an element of $R$ defined as $\operatorname{neg} (\operatorname{sumFrom} (n , i + 1 , \lambda k . F (k , k)))\times \operatorname{get} (n , A , i , j)+ \operatorname{sumFrom} (n , i + 1 , \lambda k_{1} . F (i , k_{1})\times \operatorname{get} (n , A , k_{1} , j))$.

BirdDet.sumFromdefMathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs, function or constant

Wording

no wording

English

Let $n$ and $\mathrm{lo}$ be natural numbers. Let $f$ be a function from natural numbers to elements of $R$. Then $\operatorname{sumFrom}$ applied to $n$, $\mathrm{lo}$ and $f$ is an element of $R$ defined as $\mathrm{BirdDet\_\_sumFrom\_\_\_unary}$ applied to $n$, $f$ and $\mathrm{lo}$.

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyNonneg

Matrix.IsTotallyNonnegdefMathlib.LinearAlgebra.Matrix.Determinant.TotallyNonneg, predicate

Wording

M is totally nonnegative (from the docstring)

English

generation took over the time limit

Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Matrix.IsTotallyUnimodulardefMathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular, predicate

Wording

A is totally unimodular (from the name)

English

generation took over the time limit

Mathlib.LinearAlgebra.Matrix.Dual

dotProductEquivdefMathlib.LinearAlgebra.Matrix.Dual, function or constant

Wording

the dot product of R and n (from the docstring)

English

Let $R$ and $n$ be sets. Then the dot product of $R$ and $n$ is a linear equivalence of the set of functions from elements of $n$ to elements of $R$ and the set of duals of $R$ and the set of functions from elements of $n$ to elements of $R$.

Mathlib.LinearAlgebra.Matrix.DualNumber

Matrix.dualNumberEquivdefMathlib.LinearAlgebra.Matrix.DualNumber, function or constant

Wording

the dual number equivalence (from the name)

English

The dual number equivalence is an algebra isomorphism of the set of matrixes of $n$ and the set of dual numbers of $R$ and the set of dual numbers of the set of matrixes of $n$ and $R$.

Mathlib.LinearAlgebra.Matrix.Echelon.Basic

Matrix.IsLeadingEntrydefMathlib.LinearAlgebra.Matrix.Echelon.Basic, predicate

Wording

no wording

English

Let $A$ be a matrix of $n$ and $R$. Let $i$ be an element of $m$. Let $c$ be an element of $n$. Then $\operatorname{IsLeadingEntry}$ holds for $A$, $i$ and $c$, if for all elements $j$ of $n$, if $j < c$, then $\EqtMACRoH {A (i , j)}{0}$ and $A (i , c)\neq 0$.

Matrix.IsReducedRowEchelonstructureMathlib.LinearAlgebra.Matrix.Echelon.Basic, predicate

Wording

A is a reduced row echelon (from the name)

English

Let $A$ be a matrix of $n$ and $R$. Then we can say that $A$ is a reduced row echelon.

Matrix.IsRowEchelondefMathlib.LinearAlgebra.Matrix.Echelon.Basic, predicate

Wording

A is a row echelon (from the name)

English

Let $A$ be a matrix of $n$ and $R$. Then $A$ is a row echelon, if for all elements $x_{3}$ and $x_{4}$ of $m$, if $x_{3} < x_{4}$, then for all elements $x_{5}$ of $n$, if for all elements $x_{6}$ of $n$, if $x_{6} < x_{5}$, then $\EqtMACRoH {A (x_{3} , x_{6})}{0}$, then $\EqtMACRoH {A (x_{4} , x_{5})}{0}$.

Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Echelon.DecompositionstructureMathlib.LinearAlgebra.Matrix.Echelon.Decomposition, predicate

Wording

no wording

English

Let $A$ be a matrix of $n$ and $R$. Let $L$ be a matrix of $m$ and $R$. Let $x_{4}$ be a permutation of $m$. Let $\mathrm{pivot}$ be a function from elements of $m$ to elements of $\mathrm{WithTop}$ applied to $n$. Then we can say that $\operatorname{Decomposition}$ holds for $A$, $L$, $x_{4}$ and $\mathrm{pivot}$.

Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Matrix.IsPivotedBystructureMathlib.LinearAlgebra.Matrix.Echelon.Pivot, predicate

Wording

no wording

English

Let $A$ be a matrix of $n$ and $R$. Let $l$ be a function from elements of $m$ to elements of $\mathrm{WithTop}$ applied to $n$. Then we can say that $\operatorname{IsPivotedBy}$ holds for $A$ and $l$.

Mathlib.LinearAlgebra.Matrix.ElementaryRowOperations

Matrix.GeneralLinearGroup.rowScaledefMathlib.LinearAlgebra.Matrix.ElementaryRowOperations, function or constant

Wording

the row scale of i and c (from the name)

English

Let $i$ be an element of $m$. Let $c$ be a unit of $R$. Then the row scale of $i$ and $c$ is a general linear group of $m$ and $R$.

Matrix.GeneralLinearGroup.transvectiondefMathlib.LinearAlgebra.Matrix.ElementaryRowOperations, function or constant

Wording

the transvection of j and c (from the name)

English

Let $i$ and $j$ be elements of $m$ such that $i \neq j$. Let $c$ be an element of $R$. Then the transvection of $j$ and $c$ is a general linear group of $m$ and $R$.

Matrix.RowEquivalentdefMathlib.LinearAlgebra.Matrix.ElementaryRowOperations, predicate

Wording

A is a row equivalent with respect to B (from the name)

English

Let $A$ and $B$ be matrixes of $n$ and $R$. Then $A$ is a row equivalent with respect to $B$, if $B$ is an element of the orbit of the set of general linear groups of $m$ and $R$ and $A$.

Matrix.rowScaledefMathlib.LinearAlgebra.Matrix.ElementaryRowOperations, function or constant

Wording

the row scale of i and c (from the name)

English

Let $i$ be an element of $m$. Let $c$ be an element of $R$. Then the row scale of $i$ and $c$ is a matrix of $m$ and $R$ defined as the diagonal of $\operatorname{mulSingle}$ applied to $i$ and $c$.

Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

FixedDetMatrices.reducedefMathlib.LinearAlgebra.Matrix.FixedDetMatrices, function or constant

Wording

no wording

English

Let $x$ be a fixed determinant matrix of $\Integer$ and $m$. Then $\operatorname{reduce}$ applied to $x$ is a fixed determinant matrix of $\Integer$ and $m$.

FixedDetMatrices.reduceStepdefMathlib.LinearAlgebra.Matrix.FixedDetMatrices, function or constant

Wording

no wording

English

Let $A$ be a fixed determinant matrix of $\Integer$ and $m$. Then $\operatorname{reduceStep}$ applied to $A$ is a fixed determinant matrix of $\Integer$ and $m$ defined as $\HSMulhSMulMACRoAL {\operatorname{S}}{(\HSMulhSMulMACRoAL {(\operatorname{T} ^ {\operatorname{neg} (\frac{ 0}{0})})}{A})}$.

FixedDetMatrices.reduce_recdefMathlib.LinearAlgebra.Matrix.FixedDetMatrices, function or constant

Wording

no wording

English

Let $\mathrm{base}$ be a function from fixed determinant matrixes $A_{2}$ of $\Integer$ and $m$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Eq} (0 , 0)$ to elements of $C$ applied to $A_{2}$. Let $\mathrm{step}$ be a function from fixed determinant matrixes $A_{1}$ of $\Integer$ and $m$ and elements of $\mathrm{Proof}$ applied to $\mathrm{Neq} (0 , 0)$ and elements of $C$ applied to $\operatorname{reduceStep}$ applied to $A_{1}$ to elements of $C$ applied to $A_{1}$. Let $A$ be a fixed determinant matrix of $\Integer$ and $m$. Then $\mathrm{FixedDetMatrices\_\_reduce\_rec}$ applied to $A_{2}$, $\mathrm{base}$, $A_{1}$, $\mathrm{step}$ and $A$ is an element of $C$ applied to $A$.

FixedDetMatrices.repsdefMathlib.LinearAlgebra.Matrix.FixedDetMatrices, function or constant

Wording

no wording

English

Let $m$ be an integer. Then $\operatorname{reps}$ applied to $m$ is an element of the power set of the set of fixed determinant matrixes of $\Integer$ and $m$ defined as $\operatorname{ofPred}$ applied to the function that maps $A$ to the proposition that $0 = 0 < 0 \leq 1$ and the absolute value of $1$ is less than the absolute value of $1$.

FixedDetMatrixdefMathlib.LinearAlgebra.Matrix.FixedDetMatrices, type

Wording

fixed determinant matrix of R and m (from the name)

English

Let $n$ and $R$ be sets. Let $m$ be an element of $R$. Then a fixed determinant matrix of $R$ and $m$ is an element of the function that maps $n$, $R$ and $m$ to $\SubtypeSet {A}{(\EqtMACRoH {\operatorname{det} (A)}{m})}$.

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic

Matrix.planeConformalMatrixdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic, function or constant

Wording

the plane conformal matrix of a and b (from the name)

English

Let $a$ and $b$ be elements of $R$ such that $a ^ {2}+ b ^ {2}\neq 0$. Then the plane conformal matrix of $a$ and $b$ is a general linear group of $\mathrm{Fin}$ applied to $2$ and $R$.

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card

Matrix.equiv_GL_linearindependentdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\mathrm{Matrix\_\_equiv\_GL\_linearindependent}$ applied to $n$ is an equivalence from the set of general linear groups of $\mathrm{Fin}$ applied to $n$ and $x$ to $\SubtypeSet {s}{\mathrm{LinearIndependent} (x , s)}$.

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

Matrix.GLPosdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $n$ and $R$ be sets. Then $\operatorname{GLPos}$ applied to $n$ and $R$ is a subgroup of the set of general linear groups of $n$ and $R$ defined as the preimage of the determinant and the positive part subgroup of $R$.

Matrix.GeneralLinearGroupdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, type

Wording

general linear group of n and R (from the name)

English

Let $n$ and $R$ be sets. Then a general linear group of $n$ and $R$ is an element of the function that maps $n$ and $R$ to the set of units of the set of matrixes of $n$ and $R$.

Matrix.GeneralLinearGroup.detdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

the determinant (from the docstring)

English

The determinant is a monoid homomorphism of the set of general linear groups of $n$ and $R$ and $\UnitsMACRoAO {R}$.

Matrix.GeneralLinearGroup.kroneckerdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $x_{5}$ be a general linear group of $n$ and $R$. Let $y$ be a general linear group of $m$ and $R$. Then $\operatorname{kronecker}$ applied to $x_{5}$ and $y$ is a general linear group of $\mathrm{Prod}$ applied to $n$ and $m$ and $R$.

Matrix.GeneralLinearGroup.mapdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

the map of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the map of $f$ is a monoid homomorphism of the set of general linear groups of $n$ and $R$ and the set of general linear groups of $n$ and $S$ defined as the map of $\operatorname{toMonoidHom}$ applied to the map matrix of $f$.

Matrix.GeneralLinearGroup.mk'defMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $n$ and $R$ such that the determinant of $A$ is invertible. Then $\operatorname{mk'}$ applied to $A$ and $x_{3}$ is a general linear group of $n$ and $R$ defined as the unit of $A$.

Matrix.GeneralLinearGroup.mk''defMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $n$ and $R$ such that the determinant of $A$ is a unit. Then $\operatorname{mk''}$ applied to $A$ and $h$ is a general linear group of $n$ and $R$ defined as $\operatorname{nonsingInvUnit}$ applied to $A$ and $h$.

Matrix.GeneralLinearGroup.mkOfDetNeZerodefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $A$ be a matrix of $n$ and $K$ such that the determinant of $A$ is distinct from $0$. Then $\operatorname{mkOfDetNeZero}$ applied to $A$ and $h$ is a general linear group of $n$ and $K$ defined as $\operatorname{mk'}$ applied to $A$ and $\mathrm{invertibleOfNonzero}$ applied to $h$.

Matrix.GeneralLinearGroup.scalardefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

the scalar of n (from the name)

English

Let $n$ be a set. Then the scalar of $n$ is a monoid homomorphism of $\UnitsMACRoAO {R}$ and the set of general linear groups of $n$ and $R$ defined as the map of $\operatorname{toMonoidHom}$ applied to the scalar of $n$.

Matrix.GeneralLinearGroup.toLindefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

$\operatorname{toLin}$ is a multiplicative equivalence of the set of general linear groups of $n$ and $R$ and the set of general linear groups of $R$ and the set of functions from elements of $n$ to elements of $R$ defined as the map equivalence of the multiplicative equivalence of the linear algebra isomorphism.

Matrix.GeneralLinearGroup.toLin'defMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $b$ be a basis of $R$ and $V$. Then $\operatorname{toLin'}$ applied to $b$ is a multiplicative equivalence of the set of general linear groups of $n$ and $R$ and the set of general linear groups of $R$ and $V$ defined as the composition of $\operatorname{toLin}$ and the congruence linear equivalence of the inverse of the equivalence function of $b$.

Matrix.SpecialLinearGroup.mapGLdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

Let $S$ be a set. Then $\operatorname{mapGL}$ applied to $S$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and the set of general linear groups of $n$ and $S$ defined as the composition of $\operatorname{toGL}$ and the map of the algebra map of $R$ and $S$.

Matrix.SpecialLinearGroup.toGLdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

$\operatorname{toGL}$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and the set of general linear groups of $n$ and $R$.

Matrix.SpecialLinearGroup.toGLKerEquivdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

$\operatorname{toGLKerEquiv}$ is a multiplicative equivalence of the set of special linear groups of $n$ and $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{det})}{x_{3}})}$.

Matrix.SpecialLinearGroup.toGLPosdefMathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs, function or constant

Wording

no wording

English

$\operatorname{toGLPos}$ is a monoid homomorphism of the set of special linear groups of $n$ and $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{GLPos} (n , R)}{x_{4}})}$.