Definitions: Mathlib.Algebra, part 13 of 17

AddEquiv.toLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence of e and h (from the name)

English

Let $e$ be an additive equivalence of $M$ and $x$ such that for all elements $c$ of $R$, for all elements $x_{6}$ of $M$, $\EqtMACRoH {e (\HSMulhSMulMACRoAL {c}{x_{6}})}{\HSMulhSMulMACRoAL {c}{e (x_{6})}}$. Then the linear equivalence of $e$ and $h$ is a linear equivalence of $M$ and $x$.

AddEquiv.toNatLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the natural linear equivalence of e (from the name)

English

Let $e$ be an additive equivalence of $M$ and $x$. Then the natural linear equivalence of $e$ is a linear equivalence of $M$ and $x$.

DistribMulAction.toLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence of s (from the name)

English

Let $R$ and $M$ be sets. Let $s$ be an element of $S$. Then the linear equivalence of $s$ is a linear equivalence of $M$ and $M$.

DistribMulAction.toModuleAutdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the module automorphism of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the module automorphism of $R$ and $M$ is a monoid homomorphism of $S$ and the set of linear equivalences of $M$ and $M$.

Equiv.toLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence of e and h (from the name)

English

Let $e$ be an equivalence from $M$ to $x$ such that $\operatorname{coe}$ applied to $e$ is a linear map. Then the linear equivalence of $e$ and $h$ is a linear equivalence of $M$ and $x$.

LinearEquiv.arrowCongrdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the arrow congruence of x28 and x29 (from the name)

English

Let $x_{28}$ be a linear equivalence of $x_{4}$ and $x_{5}$. Let $x_{29}$ be a linear equivalence of $x_{6}$ and $x_{7}$. Then the arrow congruence of $x_{28}$ and $x_{29}$ is a linear equivalence of the set of linear maps of $x_{4}$ and $x_{6}$ and the set of linear maps of $x_{5}$ and $x_{7}$.

LinearEquiv.arrowCongrAddEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the arrow congruence additive equivalence of x28 and x29 (from the name)

English

Let $x_{28}$ be a linear equivalence of $x_{4}$ and $x_{5}$. Let $x_{29}$ be a linear equivalence of $x_{6}$ and $x_{7}$. Then the arrow congruence additive equivalence of $x_{28}$ and $x_{29}$ is an additive equivalence of the set of linear maps of $x_{4}$ and $x_{6}$ and the set of linear maps of $x_{5}$ and $x_{7}$.

LinearEquiv.automorphismGroup.toLinearMapMonoidHomdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear map monoid homomorphism (from the name)

English

The linear map monoid homomorphism is a monoid homomorphism of the set of linear equivalences of $M$ and $M$ and the set of linear maps of $M$ and $M$.

LinearEquiv.congrLeftdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the left congruence of e (from the name)

English

Let $M$ and $S$ be sets. Let $e$ be a linear equivalence of $x$ and $x_{1}$. Then the left congruence of $e$ is a linear equivalence of the set of linear maps of $x$ and $M$ and the set of linear maps of $x_{1}$ and $M$.

LinearEquiv.congrRightdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the right congruence of f (from the name)

English

Let $f$ be a linear equivalence of $x$ and $x_{1}$. Then the right congruence of $f$ is a linear equivalence of the set of linear maps of $M$ and $x$ and the set of linear maps of $M$ and $x_{1}$ defined as the arrow congruence of the identity map of $R$ and $M$ and $f$.

LinearEquiv.conjdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the conjugate of e (from the name)

English

Let $e$ be a linear equivalence of $x_{2}$ and $x_{3}$. Then the conjugate of $e$ is a linear equivalence of the set of ends of $x$ and $x_{2}$ and the set of ends of $x_{1}$ and $x_{3}$ defined as the arrow congruence of $e$ and $e$.

LinearEquiv.conjRingEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the conjugate ring isomorphism of e (from the name)

English

Let $e$ be a linear equivalence of $x_{2}$ and $x_{3}$. Then the conjugate ring isomorphism of $e$ is a ring isomorphism of the set of ends of $x$ and $x_{2}$ and the set of ends of $x_{1}$ and $x_{3}$.

LinearEquiv.currydefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the curry of V and x3 (from the name)

English

Let $R$, $M$, $V$ and $x_{3}$ be sets. Then the curry of $V$ and $x_{3}$ is a linear equivalence of the set of functions from elements of $\mathrm{Prod}$ applied to $V$ and $x_{3}$ to elements of $M$ and the set of functions from elements of $V$ and elements of $x_{3}$ to elements of $M$.

LinearEquiv.domMulActCongrRightdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

no wording

English

Let $x_{21}$ be a linear equivalence of $x_{4}$ and $x_{5}$. Then $\operatorname{domMulActCongrRight}$ applied to $x_{21}$ is a linear equivalence of the set of linear maps of $x_{3}$ and $x_{4}$ and the set of linear maps of $x_{3}$ and $x_{5}$.

LinearEquiv.funCongrLeftdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the left function congruence of e (from the name)

English

Let $R$ and $M$ be sets. Let $e$ be an equivalence from $m$ to $n$. Then the left function congruence of $e$ is a linear equivalence of the set of functions from elements of $n$ to elements of $M$ and the set of functions from elements of $m$ to elements of $M$.

LinearEquiv.negdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the negation of R (from the name)

English

Let $R$ be a set. Then the negation of $R$ is a linear equivalence of $M$ and $M$.

LinearEquiv.ofLinearMapdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence of f and g (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $g$ be a linear map of $x_{1}$ and $M$ such that the composition of $f$ and $g$ is equal to the identity and the composition of $g$ and $f$ is equal to the identity. Then the linear equivalence of $f$ and $g$ is a linear equivalence of $M$ and $x_{1}$.

LinearEquiv.ofSubsingletondefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

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

English

Let $M$ and $x$ be sets. Then the linear equivalence of $M$ and $x$ is a linear equivalence of $M$ and $x$.

LinearEquiv.piUniquedefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the product of R and f (from the docstring)

English

Let $R$ be a set. Let $f$ be a function from elements of $x$ to sets. Then the product of $R$ and $f$ is a linear equivalence of the set of functions from elements $t$ of $x$ to elements of $f$ applied to $t$ and $f$ applied to $\operatorname{default}$.

LinearEquiv.restrictScalarsdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

no wording

English

Let $R$ be a set. Let $f$ be a linear equivalence of $M$ and $x$. Then $\operatorname{restrictScalars}$ applied to $R$ and $f$ is a linear equivalence of $M$ and $x$.

LinearEquiv.smulOfNeZerodefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the scalar multiple of a (from the name)

English

Let $K$ and $M$ be sets. Let $a$ be an element of $K$ such that $a \neq 0$. Then the scalar multiple of $a$ is a linear equivalence of $M$ and $M$ defined as the scalar multiple of $\operatorname{mk0}$ applied to $a$ and $\mathrm{ha}$.

LinearEquiv.smulOfUnitdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the scalar multiple of a (from the name)

English

Let $a$ be a unit of $R$. Then the scalar multiple of $a$ is a linear equivalence of $M$ and $M$ defined as the linear equivalence of $a$.

LinearEquiv.sumPiEquivProdPidefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the sum product equivalence product product of A (from the name)

English

Let $R$, $S$ and $T$ be sets. Let $A$ be a function from elements of $\mathrm{Sum}$ applied to $S$ and $T$ to sets. Then the sum product equivalence product product of $A$ is a linear equivalence of the set of functions from elements $\mathrm{st}$ of $\mathrm{Sum}$ applied to $S$ and $T$ to elements of $A$ applied to $\mathrm{st}$ and $\mathrm{Prod}$ applied to the set of functions from elements $s$ of $S$ to elements of $A$ applied to $\operatorname{inl}$ applied to $s$ and the set of functions from elements $t$ of $T$ to elements of $A$ applied to $\operatorname{inr}$ applied to $t$.

LinearMap.funLeftdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the left function of f (from the name)

English

Let $R$ and $M$ be sets. Let $f$ be a function from elements of $m$ to elements of $n$. Then the left function of $f$ is a linear map of the set of functions from elements of $n$ to elements of $M$ and the set of functions from elements of $m$ to elements of $M$.

LinearMap.piApplydefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

no wording

English

$\operatorname{piApply}$ is a linear map of the set of functions from elements $x_{3}$ of $M$ to linear maps of $V$ applied to $x_{3}$ and $R$ and the set of linear maps of the set of functions from elements $x_{4}$ of $M$ to elements of $V$ applied to $x_{4}$ and the set of functions from elements of $M$ to elements of $R$.

LinearMap.ringLmapEquivSelfdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Then $\operatorname{ringLmapEquivSelf}$ applied to $R$, $S$ and $M$ is a linear equivalence of the set of linear maps of $R$ and $M$ and $M$.

Module.compHom.toLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the linear equivalence of g (from the name)

English

Let $g$ be a ring isomorphism of $R$ and $S$. Then the linear equivalence of $g$ is a linear equivalence of $R$ and $S$.

Units.mulLeftLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the multiplicative left linear equivalence of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the multiplicative left linear equivalence of $R$ and $A$ is a monoid homomorphism of $\UnitsMACRoAO {A}$ and the set of linear equivalences of $A$ and $A$.

Units.mulRightLinearEquivdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the multiplicative right linear equivalence of R and a (from the name)

English

Let $R$ be a set. Let $a$ be a unit of $A$. Then the multiplicative right linear equivalence of $R$ and $a$ is a linear equivalence of $A$ and $A$.

addMonoidEndRingEquivIntdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the additive monoid end ring isomorphism integer of A (from the name)

English

Let $A$ be a set. Then the additive monoid end ring isomorphism integer of $A$ is a ring isomorphism of the set of ends of $A$ and the set of ends of $\Integer$ and $A$.

addMonoidHomLequivIntdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the additive monoid homomorphism linear equivalence integer of R (from the name)

English

Let $R$ be a set. Then the additive monoid homomorphism linear equivalence integer of $R$ is a linear equivalence of the set of additive monoid homomorphisms of $A$ and $B$ and the set of linear maps of $A$ and $B$.

addMonoidHomLequivNatdefMathlib.Algebra.Module.Equiv.Basic, function or constant

Wording

the additive monoid homomorphism linear equivalence natural number of R (from the name)

English

Let $R$ be a set. Then the additive monoid homomorphism linear equivalence natural number of $R$ is a linear equivalence of the set of additive monoid homomorphisms of $A$ and $B$ and the set of linear maps of $A$ and $B$.

Mathlib.Algebra.Module.Equiv.Defs

LinearEquivstructureMathlib.Algebra.Module.Equiv.Defs, type

Wording

linear equivalence of M and x4 (from the name)

English

Let $x_{2}$ be a ring homomorphism of $R$ and $S$. Let $M$ and $x_{4}$ be sets. Then the linear equivalences of $M$ and $x_{4}$ are a basic type.

LinearEquiv.castdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the cast of h (from the name)

English

Assume that $\EqtMACRoH {i}{j}$. Then the cast of $h$ is a linear equivalence of $M$ applied to $i$ and $M$ applied to $j$.

LinearEquiv.invFundefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the inverse function of self and x9 (from the name)

English

Let $\mathrm{self}$ be a linear equivalence of $M$ and $x_{4}$. Let $x_{9}$ be an element of $x_{4}$. Then the inverse function of $\mathrm{self}$ and $x_{9}$ is an element of $M$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{9}$.

LinearEquiv.ofInvolutivedefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the linear equivalence of f and hf (from the name)

English

Let $f$ be a linear map of $M$ and $M$ such that $\operatorname{coe}$ applied to $f$ is involutive. Then the linear equivalence of $f$ and $\mathrm{hf}$ is a linear equivalence of $M$ and $M$ defined as $\operatorname{mk}$ applied to $f$, $\operatorname{invFun}$ applied to the permutation of $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the permutation of $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the permutation of $\operatorname{coe}$ applied to $f$ and $\mathrm{hf}$.

LinearEquiv.refldefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the identity map of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the identity map of $R$ and $M$ is a linear equivalence of $M$ and $M$ defined as $\operatorname{mk}$ applied to the identity, $\operatorname{invFun}$ applied to the identity of $M$, $\mathrm{Equiv\_\_left\_inv}$ applied to the identity of $M$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the identity of $M$.

LinearEquiv.symmdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be a linear equivalence of $M$ and $x$. Then the inverse of $e$ is a linear equivalence of $x$ and $M$.

LinearEquiv.symmEquivdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the inverse equivalence (from the name)

English

The inverse equivalence is an equivalence from the set of linear equivalences of $M$ and $x$ to the set of linear equivalences of $x$ and $M$.

LinearEquiv.toAddEquivdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the additive equivalence of self (from the name)

English

Let $\mathrm{self}$ be a linear equivalence of $M$ and $x_{4}$. Then the additive equivalence of $\mathrm{self}$ is an additive equivalence of $M$ and $x_{4}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\mathrm{self}$, $\operatorname{invFun}$ applied to $\mathrm{self}$, $\mathrm{LinearEquiv\_\_left\_inv}$ applied to $\mathrm{self}$ and $\mathrm{LinearEquiv\_\_right\_inv}$ applied to $\mathrm{self}$ and $\mathrm{AddHom\_\_map\_add'}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\mathrm{self}$.

LinearEquiv.toEquivdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be a linear equivalence of $M$ and $x$. Then the equivalence of $e$ is an equivalence from $M$ to $x$ defined as $\operatorname{toEquiv}$ applied to the additive equivalence of $e$.

LinearEquiv.transdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the composition of x21 and x22 (from the name)

English

Let $x_{21}$ be a linear equivalence of $x_{3}$ and $x_{4}$. Let $x_{22}$ be a linear equivalence of $x_{4}$ and $x_{5}$. Then the composition of $x_{21}$ and $x_{22}$ is a linear equivalence of $x_{3}$ and $x_{5}$ defined as $\operatorname{mk}$ applied to the composition of $\operatorname{toLinearMap}$ applied to $x_{22}$ and $\operatorname{toLinearMap}$ applied to $x_{21}$, $\operatorname{invFun}$ applied to the composition of the equivalence of $x_{21}$ and the equivalence of $x_{22}$, $\mathrm{Equiv\_\_left\_inv}$ applied to the composition of the equivalence of $x_{21}$ and the equivalence of $x_{22}$ and $\mathrm{Equiv\_\_right\_inv}$ applied to the composition of the equivalence of $x_{21}$ and the equivalence of $x_{22}$.

LinearEquiv.transNotationdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the composition notation (from the name)

English

generation took over the time limit

LinearEquivClassdefMathlib.Algebra.Module.Equiv.Defs, predicate

Wording

no wording

English

Let $F$ be a set. Let $R$, $M$ and $x$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then $\mathrm{LinearEquivClass}$ holds for $F$, $R$, $M$ and $x$, if $\mathrm{SemilinearEquivClass}$ holds for $F$, the identity ring homomorphism of $R$, $M$ and $x$.

RingEquiv.toSemilinearEquivdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the semilinear equivalence of f (from the name)

English

Let $f$ be a ring isomorphism of $R$ and $S$. Then the semilinear equivalence of $f$ is a linear equivalence of $R$ and $S$.

SemilinearEquivClassclassMathlib.Algebra.Module.Equiv.Defs, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $S$. Let $M$ and $x_{4}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SemilinearEquivClass}$ holds for $F$, $x_{2}$, $M$ and $x_{4}$.

SemilinearEquivClass.semilinearEquivdefMathlib.Algebra.Module.Equiv.Defs, function or constant

Wording

the semilinear equivalence of f (from the name)

English

Let $f$ be an element of $F$. Then the semilinear equivalence of $f$ is a linear equivalence of $M$ and $x$.

Mathlib.Algebra.Module.Equiv.Opposite

MulOpposite.opLinearEquivdefMathlib.Algebra.Module.Equiv.Opposite, function or constant

Wording

the opposite linear equivalence of R (from the name)

English

Let $R$ be a set. Then the opposite linear equivalence of $R$ is a linear equivalence of $M$ and the set of multiplicative opposites of $M$.

Mathlib.Algebra.Module.FinitePresentation

Module.FinitePresentationclassMathlib.Algebra.Module.FinitePresentation, predicate

Wording

no wording

English

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

Module.FinitePresentation.linearEquivMapdefMathlib.Algebra.Module.FinitePresentation, function or constant

Wording

the linear equivalence map of S (from the name)

English

Let $S$ be a submonoid of $R$. Then the linear equivalence map of $S$ is a linear equivalence of the set of localized modules of $S$ and the set of linear maps of $M$ and $N$ and the set of linear maps of the set of localized modules of $S$ and $M$ and the set of localized modules of $S$ and $N$ defined as the linear equivalence of the linear map of $S$ and the set of linear maps of $M$ and $N$ and the map of the linear map of $S$ and $M$ and the linear map of $S$ and $N$.

Module.FinitePresentation.linearEquivMapExtendScalarsdefMathlib.Algebra.Module.FinitePresentation, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Then $\operatorname{linearEquivMapExtendScalars}$ applied to $S$ is a linear equivalence of the set of localized modules of $S$ and the set of linear maps of $M$ and $N$ and the set of linear maps of the set of localized modules of $S$ and $M$ and the set of localized modules of $S$ and $N$ defined as the linear equivalence of the linear map of $S$ and the set of linear maps of $M$ and $N$ and $\operatorname{mapExtendScalars}$ applied to $S$, the linear map of $S$ and $M$, the linear map of $S$ and $N$ and the set of localizations of $S$.

Mathlib.Algebra.Module.GradedModule

DirectSum.GdistribMulActionclassMathlib.Algebra.Module.GradedModule, predicate

Wording

no wording

English

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then we can say that $\operatorname{GdistribMulAction}$ holds for $A$ and $M$.

DirectSum.GmoduleclassMathlib.Algebra.Module.GradedModule, predicate

Wording

no wording

English

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then we can say that $\operatorname{Gmodule}$ holds for $A$ and $M$.

DirectSum.Gmodule.smulAddMonoidHomdefMathlib.Algebra.Module.GradedModule, function or constant

Wording

the scalar multiple additive monoid homomorphism of A and M (from the name)

English

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then the scalar multiple additive monoid homomorphism of $A$ and $M$ is an additive monoid homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $A$ applied to $i$ and the set of additive monoid homomorphisms of the set of direct sums of $x_{1}$ and the function that maps $i_{1}$ to $M$ applied to $i_{1}$ and the set of direct sums of $x_{1}$ and the function that maps $i_{2}$ to $M$ applied to $i_{2}$ defined as the additive monoid of the function that maps $\mathrm{\_i}$ to the flip of the additive monoid of the function that maps $\mathrm{\_j}$ to the flip of the composition of $\operatorname{compHom}$ applied to $\operatorname{of}$ applied to $M$ and the sum of $\mathrm{\_i}$ and $\mathrm{\_j}$ and $\operatorname{gsmulHom}$ applied to $A$ and $M$.

DirectSum.gsmulHomdefMathlib.Algebra.Module.GradedModule, function or constant

Wording

no wording

English

Let $A$ be a function from elements of $x$ to sets. Let $M$ be a function from elements of $x_{1}$ to sets. Then $\operatorname{gsmulHom}$ applied to $A$ and $M$ is an additive monoid homomorphism of $A$ applied to $i$ and the set of additive monoid homomorphisms of $M$ applied to $j$ and $M$ applied to the sum of $i$ and $j$.

GradedModule.linearEquivdefMathlib.Algebra.Module.GradedModule, function or constant

Wording

the linear equivalence of x7 and x9 (from the name)

English

Let $x_{7}$ be a function from elements of $x$ to elements of $x_{3}$. Let $x_{9}$ be a function from elements of $x_{1}$ to elements of $x_{2}$. Then the linear equivalence of $x_{7}$ and $x_{9}$ is a linear equivalence of $M$ and the set of direct sums of $x_{1}$ and the function that maps $i$ to $\SubtypeSet {x_{17}}{(\MembershipmemMACRoT {x_{9} (i)}{x_{17}})}$.

Mathlib.Algebra.Module.Hom

AddMonoidHom.smuldefMathlib.Algebra.Module.Hom, function or constant

Wording

the scalar multiple (from the name)

English

The scalar multiple is an additive monoid homomorphism of $R$ and the set of additive monoid homomorphisms of $M$ and $M$ defined as the additive monoid homomorphism of the additive monoid end of $R$ and $M$.

Mathlib.Algebra.Module.Injective

Module.BaerdefMathlib.Algebra.Module.Injective, predicate

Wording

no wording

English

Let $R$ and $Q$ be sets. Then $\operatorname{Baer}$ holds for $R$ and $Q$, if for all ideals $I$ of $R$, for all linear maps $g$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {I}{x_{4}})}$ and $Q$, there exists a linear map $\mathrm{g'}$ of $R$ and $Q$, such that for all elements $x_{3}$ of $R$, for all elements $\mathrm{mem}$ of $\mathrm{Proof}$ applied to $\MembershipmemMACRoT {I}{x_{3}}$, $\EqtMACRoH {\mathrm{g'} (x_{3})}{g (x_{3})}$.

Module.Baer.ExtensionOfstructureMathlib.Algebra.Module.Injective, type

Wording

no wording

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Then the elements of $\operatorname{ExtensionOf}$ applied to $i$ and $f$ are a basic type.

Module.Baer.ExtensionOf.maxdefMathlib.Algebra.Module.Injective, function or constant

Wording

the maximum of hchain and hnonempty (from the name)

English

Assume that $\mathrm{IsChain}$ holds for the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{Leq} (x_{7} , x_{8})$ and $c$. Assume that $c$ is nonempty. Then the maximum of $\mathrm{hchain}$ and $\mathrm{hnonempty}$ is an element of $\operatorname{ExtensionOf}$ applied to $i$ and $f$.

Module.Baer.ExtensionOfMaxAdjoin.extendIdealTodefMathlib.Algebra.Module.Injective, function or constant

Wording

no wording

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Assume that $\operatorname{Baer}$ holds for $R$ and $Q$. Let $y$ be an element of $N$. Then $\operatorname{extendIdealTo}$ applied to $i$, $f$, $h_{1}$ and $y$ is a linear map of $R$ and $Q$.

Module.Baer.ExtensionOfMaxAdjoin.extensionToFundefMathlib.Algebra.Module.Injective, function or constant

Wording

the extension to function of f and x7 (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Assume that $\operatorname{Baer}$ holds for $R$ and $Q$. Let $x_{7}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{supExtensionOfMaxSingleton} (f , y)}{x_{8}})}$. Then the extension to function of $f$ and $x_{7}$ is an element of $Q$ defined as $\operatorname{toFun'} (\operatorname{toLinearPMap} (\operatorname{extensionOfMax} (i , f)), \operatorname{fst} (i , x_{7}))+ \operatorname{extendIdealTo} (i , f , h_{1} , y , \operatorname{snd} (i , x_{7}))$.

Module.Baer.ExtensionOfMaxAdjoin.fstdefMathlib.Algebra.Module.Injective, function or constant

Wording

the first component of i and x7 (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $x_{7}$ be an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{supExtensionOfMaxSingleton} (f , y)}{x_{9}})}$. Then the first component of $i$ and $x_{7}$ is an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{domain} (\operatorname{toLinearPMap} (\operatorname{extensionOfMax} (i , f)))}{x_{8}})}$.

Module.Baer.ExtensionOfMaxAdjoin.idealdefMathlib.Algebra.Module.Injective, function or constant

Wording

the ideal of f and y (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Let $y$ be an element of $N$. Then the ideal of $f$ and $y$ is an ideal of $R$ defined as the preimage of the right scalar multiple of the identity and $y$ and the domain of $\operatorname{toLinearPMap}$ applied to the extension of $i$ and $f$.

Module.Baer.ExtensionOfMaxAdjoin.idealTodefMathlib.Algebra.Module.Injective, function or constant

Wording

no wording

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Let $y$ be an element of $N$. Then $\operatorname{idealTo}$ applied to $i$, $f$ and $y$ is a linear map of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ideal} (f , y)}{x_{7}})}$ and $Q$.

Module.Baer.ExtensionOfMaxAdjoin.snddefMathlib.Algebra.Module.Injective, function or constant

Wording

the second component of i and x7 (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $x_{7}$ be an element of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{supExtensionOfMaxSingleton} (f , y)}{x_{8}})}$. Then the second component of $i$ and $x_{7}$ is an element of $R$.

Module.Baer.extensionOfMaxdefMathlib.Algebra.Module.Injective, function or constant

Wording

the extension of i and f (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Then the extension of $i$ and $f$ is an element of $\operatorname{ExtensionOf}$ applied to $i$ and $f$.

Module.Baer.extensionOfMaxAdjoindefMathlib.Algebra.Module.Injective, function or constant

Wording

the extension of f and y (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Assume that $\operatorname{Baer}$ holds for $R$ and $Q$. Let $y$ be an element of $N$. Then the extension of $f$ and $y$ is an element of $\operatorname{ExtensionOf}$ applied to $i$ and $f$.

Module.Baer.supExtensionOfMaxSingletondefMathlib.Algebra.Module.Injective, function or constant

Wording

the supremum extension of f and y (from the name)

English

Let $i$ be a linear map of $M$ and $N$. Let $f$ be a linear map of $M$ and $Q$. Let $y$ be an element of $N$. Then the supremum extension of $f$ and $y$ is a submodule of $R$ and $N$ defined as the maximum of the domain of $\operatorname{toLinearPMap}$ applied to the extension of $i$ and $f$ and the span of $R$ and $\operatorname{singleton}$ applied to $y$.

Module.InjectiveclassMathlib.Algebra.Module.Injective, predicate

Wording

no wording

English

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

Mathlib.Algebra.Module.Lattice

Module.Basis.extendOfIsLatticedefMathlib.Algebra.Module.Lattice, function or constant

Wording

no wording

English

Let $K$ be a set. Let $b$ be a basis of $R$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {M}{x_{7}})}$. Then $\operatorname{extendOfIsLattice}$ applied to $K$ and $b$ is a basis of $K$ and $V$.

Submodule.IsLatticeclassMathlib.Algebra.Module.Lattice, predicate

Wording

no wording

English

Let $A$ be an element of $\mathrm{outParam}$ applied to the set of sets. Let $M$ be a submodule of $R$ and $V$. Then we can say that $\operatorname{IsLattice}$ holds for $A$ and $M$.

Mathlib.Algebra.Module.LinearMap.Basic

LinearMap.ltoFundefMathlib.Algebra.Module.LinearMap.Basic, function or constant

Wording

no wording

English

Let $R$, $M$, $N$ and $A$ be sets. Then $\operatorname{ltoFun}$ applied to $R$, $M$, $N$ and $A$ is a linear map of the set of linear maps of $M$ and $N$ and the set of functions from elements of $M$ to elements of $N$.

Sum.elimZeroLeftdefMathlib.Algebra.Module.LinearMap.Basic, function or constant

Wording

the left eliminator zero (from the name)

English

The left eliminator zero is a linear map of the set of functions from elements of $x$ to elements of $R$ and the set of functions from elements of $\mathrm{Sum}$ applied to $x_{1}$ and $x$ to elements of $R$.

Sum.elimZeroRightdefMathlib.Algebra.Module.LinearMap.Basic, function or constant

Wording

the right eliminator zero (from the name)

English

The right eliminator zero is a linear map of the set of functions from elements of $x$ to elements of $R$ and the set of functions from elements of $\mathrm{Sum}$ applied to $x$ and $x_{1}$ to elements of $R$.

Mathlib.Algebra.Module.LinearMap.Defs

AddMonoidHom.toIntLinearMapdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the integer linear map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $x$. Then the integer linear map of $f$ is a linear map of $M$ and $x$.

AddMonoidHom.toNatLinearMapdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the natural linear map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $x$. Then the natural linear map of $f$ is a linear map of $M$ and $x$.

IsLinearMapstructureMathlib.Algebra.Module.LinearMap.Defs, predicate

Wording

f is a linear map (from the name)

English

Let $R$ be a set. Let $f$ be a function from elements of $M$ to elements of $x$. Then we can say that $f$ is a linear map.

IsLinearMap.mk'defMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

no wording

English

Let $f$ be a function from elements of $M$ to elements of $x$ such that $f$ is a linear map. Then $\operatorname{mk'}$ applied to $f$ and $\mathrm{lin}$ is a linear map of $M$ and $x$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $f$ and $\mathrm{IsLinearMap\_\_map\_add}$ applied to $\mathrm{lin}$ and $\mathrm{IsLinearMap\_\_map\_smul}$ applied to $\mathrm{lin}$.

LinearMapstructureMathlib.Algebra.Module.LinearMap.Defs, type

Wording

linear map of M and x3 (from the name)

English

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

LinearMap.CompatibleSMulclassMathlib.Algebra.Module.LinearMap.Defs, predicate

Wording

no wording

English

Let $M$, $x$, $R$ and $S$ be sets. Then we can say that $\operatorname{CompatibleSMul}$ holds for $M$, $x$, $R$ and $S$.

LinearMap.compdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a linear map of $x_{4}$ and $x_{5}$. Let $g$ be a linear map of $x_{3}$ and $x_{4}$. Then the composition of $f$ and $g$ is a linear map of $x_{3}$ and $x_{5}$.

LinearMap.compNotationdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the composition notation (from the name)

English

generation took over the time limit

LinearMap.copydefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the copy of f and h (from the name)

English

Let $f$ be a linear map of $M$ and $x$. Let $\mathrm{f'}$ be a function from elements of $M$ to elements of $x$ such that $\mathrm{f'}$ is equal to $\operatorname{coe}$ applied to $f$. Then the copy of $f$ and $\mathrm{f'}$ is a linear map of $M$ and $x$.

LinearMap.evalAddMonoidHomdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the evaluation additive monoid homomorphism of a (from the name)

English

Let $a$ be an element of $M$. Then the evaluation additive monoid homomorphism of $a$ is an additive monoid homomorphism of the set of linear maps of $M$ and $x_{2}$ and $x_{2}$.

LinearMap.iddefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the identity (from the name)

English

The identity is a linear map of $M$ and $M$.

LinearMap.id'defMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the identity (from the name)

English

The identity is a linear map of $M$ and $M$.

LinearMap.inversedefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a linear map of $M$ and $x$. Let $g$ be a function from elements of $x$ to elements of $M$ such that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$ and $\operatorname{RightInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the inverse of $f$ and $g$ is a linear map of $x$ and $M$.

LinearMap.mulLeftdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the multiplication on the left of R and a (from the docstring)

English

Let $R$ be a set. Let $a$ be an element of $A$. Then the multiplication on the left of $R$ and $a$ is a linear map of $A$ and $A$.

LinearMap.mulLeftRightdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the right multiplicative left of R and ab (from the name)

English

Let $R$ be a set. Let $\mathrm{ab}$ be an element of $\mathrm{Prod}$ applied to $A$ and $A$. Then the right multiplicative left of $R$ and $\mathrm{ab}$ is a linear map of $A$ and $A$ defined as the composition of the multiplication on the right of $R$ and $\ProdsndMACRoAA {\mathrm{ab}}$ and the multiplication on the left of $R$ and $\ProdfstMACRoZ {\mathrm{ab}}$.

LinearMap.mulRightdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the multiplication on the right of R and b (from the docstring)

English

Let $R$ be a set. Let $b$ be an element of $A$. Then the multiplication on the right of $R$ and $b$ is a linear map of $A$ and $A$.

LinearMap.ofClassdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the linear map of f (from the name)

English

Let $f$ be an element of $F$. Then the linear map of $f$ is a linear map of $M$ and $x$.

LinearMap.restrictScalarsdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{9}$ be a linear map of $M$ and $x$. Then $\operatorname{restrictScalars}$ applied to $R$ and $x_{9}$ is a linear map of $M$ and $x$.

LinearMap.restrictScalarsₗdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

no wording

English

Let $R$, $S$, $M$, $N$ and $x_{8}$ be sets. Then $\mathrm{LinearMap\_\_restrictScalars\_u2097\_}$ applied to $R$, $S$, $M$, $N$ and $x_{8}$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\mathrm{LinearMap\_\_restrictScalars\_add}$ and $\mathrm{LinearMap\_\_restrictScalars\_smul}$.

LinearMap.toAddMonoidHomdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the additive monoid homomorphism of f (from the name)

English

Let $f$ be a linear map of $x$ and $x_{1}$. Then the additive monoid homomorphism of $f$ is an additive monoid homomorphism of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ applied to $f$ and $\mathrm{LinearMap\_\_map\_zero}$ applied to $f$ and $\mathrm{LinearMap\_\_map\_add}$ applied to $f$.

LinearMap.toAddMonoidHom'defMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the additive monoid homomorphism (from the name)

English

The additive monoid homomorphism is an additive monoid homomorphism of the set of linear maps of $M$ and $x_{2}$ and the set of additive monoid homomorphisms of $M$ and $x_{2}$.

LinearMap.toDistribMulActionHomdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the distributive multiplicative action homomorphism of f (from the name)

English

Let $f$ be a linear map of $M$ and $x$. Then the distributive multiplicative action homomorphism of $f$ is a distributive multiplicative action homomorphism of $M$ and $x$.

LinearMap.toMulActionHomdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the multiplicative action homomorphism of self (from the name)

English

Let $\mathrm{self}$ be a linear map of $M$ and $x_{3}$. Then the multiplicative action homomorphism of $\mathrm{self}$ is a multiplicative action homomorphism of $M$ and $x_{3}$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\mathrm{self}$ and $\mathrm{LinearMap\_\_map\_smul'}$ applied to $\mathrm{self}$.

LinearMapClassdefMathlib.Algebra.Module.LinearMap.Defs, predicate

Wording

R is a linear map class (from the name)

English

Let $F$, $M$ and $x$ be sets. Let $R$ be an element of $\mathrm{outParam}$ applied to the set of sets. Then $R$ is a linear map class, if $\mathrm{SemilinearMapClass}$ holds for $F$, the identity ring homomorphism of $R$, $M$ and $x$.

Module.compHom.toLinearMapdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the linear map of g (from the name)

English

Let $g$ be a ring homomorphism of $R$ and $S$. Then the linear map of $g$ is a linear map of $R$ and $S$.

RingHom.toSemilinearMapdefMathlib.Algebra.Module.LinearMap.Defs, function or constant

Wording

the semilinear map of f (from the name)

English

Let $f$ be a ring homomorphism of $R$ and $S$. Then the semilinear map of $f$ is a linear map of $R$ and $S$.

SemilinearMapClassclassMathlib.Algebra.Module.LinearMap.Defs, predicate

Wording

no wording

English

Let $F$ be a set. Let $x_{2}$ be an element of $\mathrm{outParam}$ applied to the set of ring homomorphisms of $R$ and $S$. Let $M$ and $x_{3}$ be elements of $\mathrm{outParam}$ applied to the set of sets. Then we can say that $\mathrm{SemilinearMapClass}$ holds for $F$, $x_{2}$, $M$ and $x_{3}$.

Mathlib.Algebra.Module.LinearMap.End

DistribMulAction.toModuleEnddefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the module end of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the module end of $R$ and $M$ is a monoid homomorphism of $S$ and the set of ends of $R$ and $M$.

DistribSMul.toLinearMapdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the linear map of s (from the name)

English

Let $R$ and $M$ be sets. Let $s$ be an element of $S$. Then the linear map of $s$ is a linear map of $M$ and $M$.

LinearMap.applyₗdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

no wording

English

$\mathrm{LinearMap\_\_apply\_u2097\_}$ is a linear map of $M$ and the set of linear maps of the set of linear maps of $M$ and $x$ and $x$.

LinearMap.applyₗ'defMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

no wording

English

Let $S$ be a set. Then $\mathrm{LinearMap\_\_apply\_u2097\_'}$ applied to $S$ is an additive monoid homomorphism of $M$ and the set of linear maps of the set of linear maps of $M$ and $x$ and $x$.

LinearMap.compRightdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

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

English

Let $S$ be a set. Let $f$ be a linear map of $x$ and $x_{1}$. Then the right composition of $S$ and $f$ is a linear map of the set of linear maps of $M$ and $x$ and the set of linear maps of $M$ and $x_{1}$.

LinearMap.smulRightdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

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

English

Let $f$ be a linear map of $x$ and $S$. Let $x_{9}$ be an element of $M$. Then the right scalar multiple of $f$ and $x_{9}$ is a linear map of $x$ and $M$.

LinearMap.smulRightₗdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the right scalar multiple (from the name)

English

The right scalar multiple is a linear map of the set of linear maps of $x$ and $R$ and the set of linear maps of $M$ and the set of linear maps of $x$ and $M$.

Module.EnddefMathlib.Algebra.Module.LinearMap.End, type

Wording

end of R and M (from the name)

English

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

Module.End.smulLeftdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the left scalar multiple of x3 and h (from the name)

English

Let $x_{3}$ be an element of $R$ such that $x_{3}$ is an element of the center of $R$. Then the left scalar multiple of $x_{3}$ and $h$ is an end of $R$ and $M$.

Module.toModuleEnddefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the module end of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the module end of $R$ and $M$ is a ring homomorphism of $S$ and the set of ends of $R$ and $M$.

RingEquiv.moduleEndSelfdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the module end self of R (from the name)

English

Let $R$ be a set. Then the module end self of $R$ is a ring isomorphism of the set of multiplicative opposites of $R$ and the set of ends of $R$ and $R$.

RingEquiv.moduleEndSelfOpdefMathlib.Algebra.Module.LinearMap.End, function or constant

Wording

the module end self opposite of R (from the name)

English

Let $R$ be a set. Then the module end self opposite of $R$ is a ring isomorphism of $R$ and the set of ends of the set of multiplicative opposites of $R$ and $R$.

Mathlib.Algebra.Module.LinearMap.FiniteRange

LinearMap.HasFiniteRangedefMathlib.Algebra.Module.LinearMap.FiniteRange, predicate

Wording

f has finite ranges (from the name)

English

Let $f$ be a linear map of $V$ and $x$. Then $f$ has finite ranges, if $\operatorname{FG}$ holds for the range of $f$.

LinearMap.HasNoetherianRangedefMathlib.Algebra.Module.LinearMap.FiniteRange, predicate

Wording

f has Noetherian ranges (from the name)

English

Let $f$ be a linear map of $V$ and $x$. Then $f$ has Noetherian ranges, if $\mathrm{IsNoetherian}$ holds for $K$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{6}})}$.

LinearMap.IsLeftQuasiInversedefMathlib.Algebra.Module.LinearMap.FiniteRange, predicate

Wording

no wording

English

Let $u$ be a linear map of $V$ and $x$. Let $v$ be a linear map of $x$ and $V$. Then $\operatorname{IsLeftQuasiInverse}$ holds for $u$ and $v$, if $\operatorname{Equiv}$ holds for the composition of $u$ and $v$ and the identity.

LinearMap.IsQuasiInversedefMathlib.Algebra.Module.LinearMap.FiniteRange, predicate

Wording

no wording

English

Let $u$ be a linear map of $x_{1}$ and $x$. Let $v$ be a linear map of $x$ and $x_{1}$. Then $\operatorname{IsQuasiInverse}$ holds for $u$ and $v$, if $\operatorname{IsLeftQuasiInverse}$ holds for $u$ and $v$ and $\operatorname{IsRightQuasiInverse}$ holds for $u$ and $v$.

LinearMap.IsRightQuasiInversedefMathlib.Algebra.Module.LinearMap.FiniteRange, predicate

Wording

no wording

English

Let $u$ be a linear map of $x_{1}$ and $x$. Let $v$ be a linear map of $x$ and $x_{1}$. Then $\operatorname{IsRightQuasiInverse}$ holds for $u$ and $v$, if $\operatorname{Equiv}$ holds for the composition of $v$ and $u$ and the identity.

LinearMap.finiteRangedefMathlib.Algebra.Module.LinearMap.FiniteRange, function or constant

Wording

the finite range of V and x (from the name)

English

Let $K$, $V$ and $x$ be sets. Then the finite range of $V$ and $x$ is a submodule of $K$ and the set of linear maps of $V$ and $x$.

Mathlib.Algebra.Module.LinearMap.Index

LinearMap.indexdefMathlib.Algebra.Module.LinearMap.Index, function or constant

Wording

the index of f (from the docstring)

English

Let $f$ be a linear map of $M$ and $N$. Then the index of $f$ is an element of $\Integer$ defined as $\operatorname{finrank} (R , \SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ker} (f)}{x_{5}})})- \operatorname{finrank} (R , \operatorname{Quotient} (N , \operatorname{range} (f)))$.

Mathlib.Algebra.Module.LinearMap.Polynomial

LinearMap.IsNilRegulardefMathlib.Algebra.Module.LinearMap.Polynomial, predicate

Wording

no wording

English

Let $x_{5}$ be a linear map of $L$ and the set of ends of $R$ and $M$. Let $x_{6}$ be an element of $L$. Then $\operatorname{IsNilRegular}$ holds for $x_{5}$ and $x_{6}$, if $\operatorname{coeff}$ applied to the characteristic polynomial of $x_{5}$ applied to $x_{6}$ and $\operatorname{nilRank}$ applied to $x_{5}$ is distinct from $0$.

LinearMap.nilRankdefMathlib.Algebra.Module.LinearMap.Polynomial, function or constant

Wording

no wording

English

Let $x_{5}$ be a linear map of $L$ and the set of ends of $R$ and $M$. Then $\operatorname{nilRank}$ applied to $x_{5}$ is a natural number defined as $\operatorname{nilRankAux}$ applied to $x_{5}$ and $\operatorname{chooseBasis}$ applied to $R$ and $L$.

LinearMap.polyCharpolydefMathlib.Algebra.Module.LinearMap.Polynomial, function or constant

Wording

the polynomial characteristic polynomial of x6 and b (from the name)

English

Let $x_{6}$ be a linear map of $L$ and the set of ends of $R$ and $M$. Let $b$ be a basis of $R$ and $L$. Then the polynomial characteristic polynomial of $x_{6}$ and $b$ is a polynomial of the set of multivariate polynomials of $x$ and $R$ defined as $\operatorname{polyCharpolyAux}$ applied to $x_{6}$, $b$ and $\operatorname{chooseBasis}$ applied to $R$ and $M$.

LinearMap.toMvPolynomialdefMathlib.Algebra.Module.LinearMap.Polynomial, function or constant

Wording

the multivariate polynomial of f and i (from the name)

English

Let $x_{11}$ be a basis of $R$ and $x$. Let $x_{12}$ be a basis of $R$ and $x_{1}$. Let $f$ be a linear map of $x$ and $x_{1}$. Let $i$ be an element of $x_{3}$. Then the multivariate polynomial of $f$ and $i$ is a multivariate polynomial of $x_{2}$ and $R$ defined as the multivariate polynomial of $\operatorname{toMatrix}$ applied to $x_{11}$, $x_{12}$ and $f$ and $i$.

Matrix.toMvPolynomialdefMathlib.Algebra.Module.LinearMap.Polynomial, function or constant

Wording

the multivariate polynomial of M and i (from the name)

English

Let $M$ be a matrix of $n$ and $R$. Let $i$ be an element of $m$. Then the multivariate polynomial of $M$ and $i$ is a multivariate polynomial of $n$ and $R$ defined as $\FinsetSum {\FinsetunivMACRoAC}{j}{\operatorname{monomial} (\FinsuppsingleMACRoS {j}{1}, M (i , j))}$.

Mathlib.Algebra.Module.LinearMap.Rat

AddMonoidHom.toRatLinearMapdefMathlib.Algebra.Module.LinearMap.Rat, function or constant

Wording

the rational number linear map of f (from the name)

English

Let $f$ be an additive monoid homomorphism of $M$ and $x$. Then the rational number linear map of $f$ is a linear map of $M$ and $x$.

Mathlib.Algebra.Module.LocalizedModule.AtPrime

IsLocalizedModule.AtPrimedefMathlib.Algebra.Module.LocalizedModule.AtPrime, predicate

Wording

no wording

English

Let $P$ be an ideal of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then $\operatorname{AtPrime}$ holds for $P$ and $f$, if $\mathrm{IsLocalizedModule}$ holds for the complement of $P$ and $f$.

LocalizedModule.AtPrimedefMathlib.Algebra.Module.LocalizedModule.AtPrime, type

Wording

no wording

English

Let $P$ be an ideal of $R$. Let $M$ be a set. Then an element of $\operatorname{AtPrime}$ applied to $P$ and $M$ is an element of the function that maps $P$ and $M$ to the set of localized modules of the complement of $P$ and $M$.

Mathlib.Algebra.Module.LocalizedModule.Basic

IsLocalizedModuleclassMathlib.Algebra.Module.LocalizedModule.Basic, predicate

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then we can say that $\mathrm{IsLocalizedModule}$ holds for $S$ and $f$.

IsLocalizedModule.AwaydefMathlib.Algebra.Module.LocalizedModule.Basic, predicate

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then $\operatorname{Away}$ holds for $x_{1}$ and $f$, if $\mathrm{IsLocalizedModule}$ holds for the power of $x_{1}$ and $f$.

IsLocalizedModule.fromLocalizedModuledefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then $\operatorname{fromLocalizedModule}$ applied to $S$ and $f$ is a linear map of the set of localized modules of $S$ and $M$ and $\mathrm{M'}$.

IsLocalizedModule.fromLocalizedModule'defMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $x_{5}$ be a localized module of $S$ and $M$. Then $\operatorname{fromLocalizedModule'}$ applied to $S$, $f$ and $x_{5}$ is an element of $\mathrm{M'}$.

IsLocalizedModule.isodefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the isomorphism of S and f (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Then the isomorphism of $S$ and $f$ is a linear equivalence of the set of localized modules of $S$ and $M$ and $\mathrm{M'}$.

IsLocalizedModule.liftdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the lift of f and g (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $g$ be a linear map of $M$ and $\mathrm{M''}$. Assume that for all elements $x_{7}$ of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$, $\operatorname{algebraMap}$ applied to $R$, the set of ends of $R$ and $\mathrm{M''}$ and $x_{7}$ is a unit. Then the lift of $f$ and $g$ is a linear map of $\mathrm{M'}$ and $\mathrm{M''}$ defined as the composition of the lift of $S$ and $g$ and $\operatorname{toLinearMap}$ applied to the inverse of the isomorphism of $S$ and $f$.

IsLocalizedModule.liftOfLEdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the lift of x11 and x12 (from the name)

English

Let $x_{9}$ and $x_{10}$ be submonoids of $R$ such that $x_{9} \leq x_{10}$. Let $x_{11}$ be a linear map of $M$ and $x_{3}$. Let $x_{12}$ be a linear map of $M$ and $x_{4}$. Then the lift of $x_{11}$ and $x_{12}$ is a linear map of $x_{3}$ and $x_{4}$.

IsLocalizedModule.linearEquivdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the linear equivalence of f and g (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $g$ be a linear map of $M$ and $\mathrm{M''}$. Then the linear equivalence of $f$ and $g$ is a linear equivalence of $\mathrm{M'}$ and $\mathrm{M''}$ defined as the composition of the inverse of the isomorphism of $S$ and $f$ and the isomorphism of $S$ and $g$.

IsLocalizedModule.mapdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the map of f and g (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $g$ be a linear map of $N$ and $\mathrm{N'}$. Then the map of $f$ and $g$ is a linear map of the set of linear maps of $M$ and $N$ and the set of linear maps of $\mathrm{M'}$ and $\mathrm{N'}$.

IsLocalizedModule.mk'defMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $m$ be an element of $M$. Let $s$ be an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$. Then $\operatorname{mk'}$ applied to $f$, $m$ and $s$ is an element of $\mathrm{M'}$ defined as $\operatorname{fromLocalizedModule}$ applied to $S$, $f$ and $\operatorname{mk}$ applied to $m$ and $s$.

LocalizedModuledefMathlib.Algebra.Module.LocalizedModule.Basic, type

Wording

localized module of S and M (from the name)

English

Let $S$ be a submonoid of $R$. Let $M$ be a set. Then a localized module of $S$ and $M$ is an element of the function that maps $S$ and $M$ to $\mathrm{OreLocalization}$ applied to $S$ and $M$.

LocalizedModule.AwaydefMathlib.Algebra.Module.LocalizedModule.Basic, type

Wording

no wording

English

Let $x_{1}$ be an element of $R$. Let $M$ be a set. Then an element of $\operatorname{Away}$ applied to $x_{1}$ and $M$ is an element of the function that maps $x_{1}$ and $M$ to the set of localized modules of the power of $x_{1}$ and $M$.

LocalizedModule.divBydefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{divBy}$ applied to $s$ is a linear map of the set of localized modules of $S$ and $M$ and the set of localized modules of $S$ and $M$.

LocalizedModule.liftdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the lift of S and g (from the name)

English

Let $S$ be a submonoid of $R$. Let $g$ be a linear map of $M$ and $\mathrm{M''}$. Assume that for all elements $x_{5}$ of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, $\operatorname{algebraMap}$ applied to $R$, the set of ends of $R$ and $\mathrm{M''}$ and $x_{5}$ is a unit. Then the lift of $S$ and $g$ is a linear map of the set of localized modules of $S$ and $M$ and $\mathrm{M''}$.

LocalizedModule.lift'defMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the lift of g and x5 (from the name)

English

Let $S$ be a submonoid of $R$. Let $g$ be a linear map of $M$ and $\mathrm{M''}$. Assume that for all elements $x_{6}$ of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$, $\operatorname{algebraMap}$ applied to $R$, the set of ends of $R$ and $\mathrm{M''}$ and $x_{6}$ is a unit. Let $x_{5}$ be a localized module of $S$ and $M$. Then the lift of $g$ and $x_{5}$ is an element of $\mathrm{M''}$.

LocalizedModule.liftOfLEdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the lift of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be submonoids of $R$ such that $x_{3} \leq x_{4}$. Then the lift of $x_{3}$ and $x_{4}$ is a linear map of the set of localized modules of $x_{3}$ and $M$ and the set of localized modules of $x_{4}$ and $M$ defined as the lift of the linear map of $x_{3}$ and $M$ and the linear map of $x_{4}$ and $M$.

LocalizedModule.liftOndefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ be a localized module of $S$ and $M$. Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$ to elements of $x_{3}$ such that for all elements $p$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, for all elements $\mathrm{p'}$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, if $\operatorname{Equiv}$ holds for $p$ and $\mathrm{p'}$, then $\EqtMACRoH {f (p)}{f (\mathrm{p'})}$. Then $\operatorname{liftOn}$ applied to $x_{4}$, $f$ and $\mathrm{wd}$ is an element of $x_{3}$.

LocalizedModule.liftOn₂defMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $x_{4}$ and $y$ be localized modules of $S$ and $M$. Let $f$ be a function from elements of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {S}{x_{12}})}$ and elements of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {S}{x_{11}})}$ to elements of $x_{3}$ such that for all elements $p$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {S}{x_{8}})}$, for all elements $q$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {S}{x_{7}})}$, for all elements $\mathrm{p'}$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$, for all elements $\mathrm{q'}$ of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$, if $\operatorname{Equiv}$ holds for $p$ and $\mathrm{p'}$, then if $\operatorname{Equiv}$ holds for $q$ and $\mathrm{q'}$, then $\EqtMACRoH {f (p , q)}{f (\mathrm{p'} , \mathrm{q'})}$. Then $\mathrm{LocalizedModule\_\_liftOn\_u2082\_}$ applied to $x_{4}$, $y$, $f$ and $\mathrm{wd}$ is an element of $x_{3}$.

LocalizedModule.mkdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

no wording

English

Let $m$ be an element of $M$. Let $s$ be an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{mk}$ applied to $m$ and $s$ is a localized module of $S$ and $M$ defined as $\operatorname{oreDiv}$ applied to $m$ and $s$.

LocalizedModule.mkLinearMapdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the linear map of S and M (from the name)

English

Let $S$ be a submonoid of $R$. Let $M$ be a set. Then the linear map of $S$ and $M$ is a linear map of $M$ and the set of localized modules of $S$ and $M$.

LocalizedModule.muldefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the product of x3 and x4 (from the name)

English

Let $x_{3}$ and $x_{4}$ be localized modules of $S$ and $A$. Then the product of $x_{3}$ and $x_{4}$ is a localized module of $S$ and $A$.

LocalizedModule.numeratorRingHomdefMathlib.Algebra.Module.LocalizedModule.Basic, function or constant

Wording

the numerator ring homomorphism (from the name)

English

The numerator ring homomorphism is a ring homomorphism of $A$ and $\mathrm{OreLocalization}$ applied to $S$ and $A$.

LocalizedModule.rdefMathlib.Algebra.Module.LocalizedModule.Basic, predicate

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $M$ be a set. Let $a$ be an element of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {S}{x_{4}})}$. Let $b$ be an element of $\mathrm{Prod}$ applied to $M$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$. Then $\operatorname{r}$ holds for $S$, $M$, $a$ and $b$, if there exists an element $u$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {S}{x_{3}})}$, such that $\EqtMACRoH {\HSMulhSMulMACRoAL {u}{(\HSMulhSMulMACRoAL {\ProdsndMACRoAA {b}}{\ProdfstMACRoZ {a}})}}{\HSMulhSMulMACRoAL {u}{(\HSMulhSMulMACRoAL {\ProdsndMACRoAA {a}}{\ProdfstMACRoZ {b}})}}$.

Mathlib.Algebra.Module.LocalizedModule.Int

IsLocalizedModule.IsIntegerdefMathlib.Algebra.Module.LocalizedModule.Int, predicate

Wording

no wording

English

Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $x_{5}$ be an element of $\mathrm{M'}$. Then $\operatorname{IsInteger}$ holds for $f$ and $x_{5}$, if $x_{5}$ is an element of the range of $f$.

IsLocalizedModule.commonDenomdefMathlib.Algebra.Module.LocalizedModule.Int, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $s$ be a finite set of $x_{5}$. Let $g$ be a function from elements of $x_{5}$ to elements of $\mathrm{M'}$. Then $\operatorname{commonDenom}$ applied to $S$, $f$, $s$ and $g$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {S}{x_{6}})}$ defined as $\operatorname{choose}$ applied to $\mathrm{IsLocalizedModule\_\_exist\_integer\_multiples}$ applied to $S$, $f$, $s$ and $g$.

IsLocalizedModule.commonDenomOfFinsetdefMathlib.Algebra.Module.LocalizedModule.Int, function or constant

Wording

no wording

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $s$ be a finite set of $\mathrm{M'}$. Then $\operatorname{commonDenomOfFinset}$ applied to $S$, $f$ and $s$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {S}{x_{5}})}$ defined as $\operatorname{commonDenom}$ applied to $S$, $f$, $s$ and $\mathrm{id}$.

IsLocalizedModule.finsetIntegerMultipledefMathlib.Algebra.Module.LocalizedModule.Int, function or constant

Wording

the finite set integer multiple of f and s (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $s$ be a finite set of $\mathrm{M'}$. Then the finite set integer multiple of $f$ and $s$ is a finite set of $M$ defined as the forward image of $\operatorname{attach}$ applied to $s$ under the function that maps $t$ to the integer multiple of $\mathrm{id}$ and $t$.

IsLocalizedModule.integerMultipledefMathlib.Algebra.Module.LocalizedModule.Int, function or constant

Wording

the integer multiple of g and i (from the name)

English

Let $S$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $\mathrm{M'}$. Let $s$ be a finite set of $x_{5}$. Let $g$ be a function from elements of $x_{5}$ to elements of $\mathrm{M'}$. Let $i$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {s}{x_{6}})}$. Then the integer multiple of $g$ and $i$ is an element of $M$.

Mathlib.Algebra.Module.LocalizedModule.Submodule

LinearMap.toKerIsLocalizeddefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{f'}$ be a linear map of $P$ and $Q$. Let $g$ be a linear map of $M$ and $P$. Then $\operatorname{toKerIsLocalized}$ applied to $p$, $f$, $\mathrm{f'}$ and $g$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{ker} (g)}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{map} (p , f , \mathrm{f'} , g))}{x_{10}})}$.

Submodule.localizeddefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localization of p and #2 (from the docstring)

English

Let $p$ be a submonoid of $R$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the localization of $p$ and $\mathrm{M'}$ is a submodule of the set of localizations of $p$ and the set of localized modules of $p$ and $M$ defined as $\operatorname{localized'}$ applied to the set of localizations of $p$, $p$, the linear map of $p$ and $M$ and $\mathrm{M'}$.

Submodule.localized'defMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $S$ be a set. Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then $\operatorname{localized'}$ applied to $S$, $p$, $f$ and $\mathrm{M'}$ is a submodule of $S$ and $N$.

Submodule.localized'FrameHomdefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localized frame homomorphism of p and f (from the name)

English

Let $S$ be a set. Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Then the localized frame homomorphism of $p$ and $f$ is a frame homomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $S$ and $N$.

Submodule.localized'gidefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $S$ be a set. Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Then $\operatorname{localized'gi}$ applied to $S$, $p$ and $f$ is a Galois insertion of $\operatorname{localized'}$ applied to $S$, $p$ and $f$ and the function that maps $x_{8}$ to the preimage of $f$ and $\operatorname{restrictScalars}$ applied to $R$ and $x_{8}$.

Submodule.localizedEquivdefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the canonical isomorphism between the localization of p and #2 (from the docstring)

English

Let $p$ be a submonoid of $R$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the canonical isomorphism between the localization of $p$ and $\mathrm{M'}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{localized} (p , \mathrm{M'})}{x_{3}})}$ and the set of localized modules of $p$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{4}})}$ defined as $\operatorname{restrictScalars}$ applied to the set of localizations of $p$ and the linear equivalence of the localization map of $p$ and $\mathrm{M'}$ and the linear map of $p$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{3}})}$.

Submodule.localized₀defMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then $\mathrm{Submodule\_\_localized\_u2080\_}$ applied to $p$, $f$ and $\mathrm{M'}$ is a submodule of $R$ and $N$.

Submodule.localized₀FrameHomdefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localized frame homomorphism of p and f (from the name)

English

Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Then the localized frame homomorphism of $p$ and $f$ is a frame homomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $R$ and $N$.

Submodule.toLocalizeddefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localization map of p and #2 (from the docstring)

English

Let $p$ be a submonoid of $R$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the localization map of $p$ and $\mathrm{M'}$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{localized} (p , \mathrm{M'})}{x_{4}})}$ defined as $\operatorname{toLocalized'}$ applied to the set of localizations of $p$, $p$, the linear map of $p$ and $M$ and $\mathrm{M'}$.

Submodule.toLocalized'defMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $S$ be a set. Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then $\operatorname{toLocalized'}$ applied to $S$, $p$, $f$ and $\mathrm{M'}$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{localized'} (S , p , f , \mathrm{M'})}{x_{9}})}$ defined as $\mathrm{Submodule\_\_toLocalized\_u2080\_}$ applied to $p$, $f$ and $\mathrm{M'}$.

Submodule.toLocalizedQuotientdefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localization map of p and #2 (from the docstring)

English

Let $p$ be a submonoid of $R$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the localization map of $p$ and $\mathrm{M'}$ is a linear map of the set of quotients of $M$ and $\mathrm{M'}$ and the set of quotients of the set of localized modules of $p$ and $M$ and the localization of $p$ and $\mathrm{M'}$ defined as the localized quotient of the linear map of $p$ and $M$ and $\mathrm{M'}$.

Submodule.toLocalizedQuotient'defMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the localized quotient of f and #4 (from the name)

English

Let $S$ be a set. Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the localized quotient of $f$ and $\mathrm{M'}$ is a linear map of the set of quotients of $M$ and $\mathrm{M'}$ and the set of quotients of $N$ and $\operatorname{localized'}$ applied to $S$, $p$, $f$ and $\mathrm{M'}$.

Submodule.toLocalized₀defMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

no wording

English

Let $p$ be a submonoid of $R$. Let $f$ be a linear map of $M$ and $N$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then $\mathrm{Submodule\_\_toLocalized\_u2080\_}$ applied to $p$, $f$ and $\mathrm{M'}$ is a linear map of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{Submodule\_\_localized\_u2080\_} (p , f , \mathrm{M'})}{x_{6}})}$.

localizedQuotientEquivdefMathlib.Algebra.Module.LocalizedModule.Submodule, function or constant

Wording

the canonical isomorphism between the localization of p and #2 (from the docstring)

English

Let $p$ be a submonoid of $R$. Let $\mathrm{M'}$ be a submodule of $R$ and $M$. Then the canonical isomorphism between the localization of $p$ and $\mathrm{M'}$ is a linear equivalence of the set of quotients of the set of localized modules of $p$ and $M$ and the localization of $p$ and $\mathrm{M'}$ and the set of localized modules of $p$ and the set of quotients of $M$ and $\mathrm{M'}$ defined as $\operatorname{restrictScalars}$ applied to the set of localizations of $p$ and the linear equivalence of the localization map of $p$ and $\mathrm{M'}$ and the linear map of $p$ and the set of quotients of $M$ and $\mathrm{M'}$.

Mathlib.Algebra.Module.Presentation.Basic

Module.PresentationstructureMathlib.Algebra.Module.Presentation.Basic, type

Wording

presentation of A and M (from the name)

English

Let $A$ and $M$ be sets. Then the presentations of $A$ and $M$ are a basic type.

Module.Presentation.ofIsPresentationdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the presentation of h (from the name)

English

Assume that $\mathrm{solution}$ is a presentation. Then the presentation of $h$ is a presentation of $A$ and $M$ defined as $\operatorname{mk}$ applied to $\mathrm{relations}$, $\mathrm{solution}$ and $h$.

Module.Presentation.ofLinearEquivdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the presentation of pres and e (from the docstring)

English

Let $\mathrm{pres}$ be a presentation of $A$ and $M$. Let $e$ be a linear equivalence of $M$ and $N$. Then the presentation of $\mathrm{pres}$ and $e$ is a presentation of $A$ and $N$.

Module.RelationsstructureMathlib.Algebra.Module.Presentation.Basic, type

Wording

relation of A (from the name)

English

Let $A$ be a set. Then the relations of $A$ are a basic type.

Module.Relations.GdefMathlib.Algebra.Module.Presentation.Basic, type

Wording

no wording

English

Let $\mathrm{self}$ be a relation of $A$. Then an element of $\operatorname{G}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

Module.Relations.QuotientdefMathlib.Algebra.Module.Presentation.Basic, type

Wording

quotient of relations (from the name)

English

Let $\mathrm{relations}$ be a relation of $A$. Then a quotient of $\mathrm{relations}$ is an element of the function that maps $\mathrm{relations}$ to the set of quotients of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ and the span of $A$ and the range of $\operatorname{relation}$ applied to $\mathrm{relations}$.

Module.Relations.RdefMathlib.Algebra.Module.Presentation.Basic, type

Wording

no wording

English

Let $\mathrm{self}$ be a relation of $A$. Then an element of $\operatorname{R}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj1}$ applied to $\mathrm{self}$.

Module.Relations.SolutionstructureMathlib.Algebra.Module.Presentation.Basic, type

Wording

solution of relations and M (from the name)

English

Let $\mathrm{relations}$ be a relation of $A$. Let $M$ be a set. Then the solutions of $\mathrm{relations}$ and $M$ are a basic type.

Module.Relations.Solution.IsPresentationstructureMathlib.Algebra.Module.Presentation.Basic, predicate

Wording

solution is a presentation (from the name)

English

Let $\mathrm{solution}$ be a solution of $\mathrm{relations}$ and $M$. Then we can say that $\mathrm{solution}$ is a presentation.

Module.Relations.Solution.IsPresentation.descdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{solution}$ is a presentation. Let $s$ be a solution of $\mathrm{relations}$ and $N$. Then $\operatorname{desc}$ applied to $h$ and $s$ is a linear map of $M$ and $N$ defined as the composition of $\operatorname{fromQuotient}$ applied to $s$ and $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $h$.

Module.Relations.Solution.IsPresentation.linearEquivdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the linear equivalence of h (from the name)

English

Assume that $\mathrm{solution}$ is a presentation. Then the linear equivalence of $h$ is a linear equivalence of the set of quotients of $\mathrm{relations}$ and $M$ defined as the linear equivalence of $\operatorname{fromQuotient}$ applied to $\mathrm{solution}$ and $\operatorname{bijective}$ applied to $h$.

Module.Relations.Solution.IsPresentation.linearMapEquivdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the linear map equivalence of h (from the name)

English

Assume that $\mathrm{solution}$ is a presentation. Then the linear map equivalence of $h$ is an equivalence from the set of linear maps of $M$ and $N$ to the set of solutions of $\mathrm{relations}$ and $N$.

Module.Relations.Solution.IsPresentation.uniqdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

no wording

English

Assume that $\mathrm{solution}$ is a presentation. Assume that $\mathrm{solution'}$ is a presentation. Then $\operatorname{uniq}$ applied to $h$ and $\mathrm{h'}$ is a linear equivalence of $M$ and $N$.

Module.Relations.Solution.IsPresentationCorestructureMathlib.Algebra.Module.Presentation.Basic, type

Wording

no wording

English

Let $\mathrm{solution}$ be a solution of $\mathrm{relations}$ and $M$. Then the elements of $\operatorname{IsPresentationCore}$ applied to $\mathrm{solution}$ are a basic type.

Module.Relations.Solution.IsPresentationCore.descdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{IsPresentationCore}$ applied to $\mathrm{solution}$. Let $s$ be a solution of $\mathrm{relations}$ and $N$. Then $\operatorname{desc}$ applied to $\mathrm{self}$ and $s$ is a linear map of $M$ and $N$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $s$.

Module.Relations.Solution.IsPresentationCore.downdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

no wording

English

Let $h$ be an element of $\operatorname{IsPresentationCore}$ applied to $\mathrm{solution}$. Then $\operatorname{down}$ applied to $h$ is an element of $\operatorname{IsPresentationCore}$ applied to $\mathrm{solution}$.

Module.Relations.Solution.fromQuotientdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

no wording

English

Let $\mathrm{solution}$ be a solution of $\mathrm{relations}$ and $M$. Then $\operatorname{fromQuotient}$ applied to $\mathrm{solution}$ is a linear map of the set of quotients of $\mathrm{relations}$ and $M$ defined as the lift of the span of $A$ and the range of $\operatorname{relation}$ applied to $\mathrm{relations}$ and the projection of $\mathrm{solution}$.

Module.Relations.Solution.ofQuotientdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the solution of relations (from the name)

English

Let $\mathrm{relations}$ be a relation of $A$. Then the solution of $\mathrm{relations}$ is a solution of $\mathrm{relations}$ and the set of quotients of $\mathrm{relations}$.

Module.Relations.Solution.ofπdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the projection of x3 and h (from the name)

English

Let $x_{3}$ be a linear map of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ and $M$ such that for all elements $r$ of $\operatorname{R}$ applied to $\mathrm{relations}$, $x_{3}$ applied to the relation of $\mathrm{relations}$ and $r$ is equal to $0$. Then the projection of $x_{3}$ and $h$ is a solution of $\mathrm{relations}$ and $M$.

Module.Relations.Solution.ofπ'defMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the projection of x3 and h (from the name)

English

Let $x_{3}$ be a linear map of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ and $M$ such that the composition of $x_{3}$ and the linear map of $\mathrm{relations}$ is equal to $0$. Then the projection of $x_{3}$ and $h$ is a solution of $\mathrm{relations}$ and $M$.

Module.Relations.Solution.postcompdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the postcomposition of solution and f (from the name)

English

Let $\mathrm{solution}$ be a solution of $\mathrm{relations}$ and $M$. Let $f$ be a linear map of $M$ and $N$. Then the postcomposition of $\mathrm{solution}$ and $f$ is a solution of $\mathrm{relations}$ and $N$.

Module.Relations.Solution.vardefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the variable of self and g (from the name)

English

Let $\mathrm{self}$ be a solution of $\mathrm{relations}$ and $M$. Let $g$ be an element of $\operatorname{G}$ applied to $\mathrm{relations}$. Then the variable of $\mathrm{self}$ and $g$ is an element of $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $g$.

Module.Relations.Solution.πdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the projection of solution (from the name)

English

Let $\mathrm{solution}$ be a solution of $\mathrm{relations}$ and $M$. Then the projection of $\mathrm{solution}$ is a linear map of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ and $M$ defined as the linear combination of $A$ and $\operatorname{var}$ applied to $\mathrm{solution}$.

Module.Relations.mapdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the linear map of relations (from the docstring)

English

Let $\mathrm{relations}$ be a relation of $A$. Then the linear map of $\mathrm{relations}$ is a linear map of $\FinsuppMACRoQ {\operatorname{R} (\mathrm{relations})}{A}$ and $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ defined as the linear combination of $A$ and $\operatorname{relation}$ applied to $\mathrm{relations}$.

Module.Relations.relationdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the relation of self and r (from the name)

English

Let $\mathrm{self}$ be a relation of $A$. Let $r$ be an element of $\operatorname{R}$ applied to $\mathrm{self}$. Then the relation of $\mathrm{self}$ and $r$ is an element of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{self})}{A}$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $r$.

Module.Relations.toQuotientdefMathlib.Algebra.Module.Presentation.Basic, function or constant

Wording

the quotient of relations (from the name)

English

Let $\mathrm{relations}$ be a relation of $A$. Then the quotient of $\mathrm{relations}$ is a linear map of $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$ and the set of quotients of $\mathrm{relations}$ defined as $\operatorname{mkQ}$ applied to the span of $A$ and the range of $\operatorname{relation}$ applied to $\mathrm{relations}$.

Mathlib.Algebra.Module.Presentation.Cokernel

Module.Presentation.CokernelDatastructureMathlib.Algebra.Module.Presentation.Cokernel, type

Wording

cokernel data of f and x9 (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $f$ be a linear map of $x_{1}$ and $x_{2}$. Let $x_{9}$ be a function from elements of $x_{8}$ to elements of $x_{1}$. Then the cokernel data of $f$ and $x_{9}$ are a basic type.

Module.Presentation.CokernelData.liftdefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the lift of self and i (from the name)

English

Let $\mathrm{self}$ be a cokernel data of $f$ and $x_{9}$. Let $i$ be an element of $x_{8}$. Then the lift of $\mathrm{self}$ and $i$ is an element of $\FinsuppMACRoQ {\operatorname{G} (\operatorname{toRelations} (x_{7}))}{A}$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $i$.

Module.Presentation.CokernelData.ofSectiondefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the cokernel data of x9 and s (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $f$ be a linear map of $x_{1}$ and $x_{2}$. Let $x_{9}$ be a function from elements of $x_{8}$ to elements of $x_{1}$. Let $s$ be a function from elements of $x_{2}$ to elements of $\FinsuppMACRoQ {\operatorname{G} (\operatorname{toRelations} (x_{7}))}{A}$ such that for all elements $x_{10}$ of $x_{2}$, $\EqtMACRoH {\mathrm{Module\_\_Relations\_\_Solution\_\_\_u3c0\_\_\_app} (\operatorname{toSolution} (x_{7}), s (x_{10}))}{x_{10}}$. Then the cokernel data of $x_{9}$ and $s$ is a cokernel data of $f$ and $x_{9}$.

Module.Presentation.cokerneldefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the cokernel of x7 and data (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $\mathrm{data}$ be a cokernel data of $f$ and $x_{9}$. Assume that the span of $A$ and the range of $x_{9}$ is equal to the top. Then the cokernel of $x_{7}$ and $\mathrm{data}$ is a presentation of $A$ and the set of quotients of $x_{2}$ and the range of $f$ defined as the presentation of $\operatorname{isPresentation}$ applied to $x_{7}$, $\mathrm{data}$ and $h$.

Module.Presentation.cokernelRelationsdefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the cokernel relation of x7 and data (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $\mathrm{data}$ be a cokernel data of $f$ and $x_{9}$. Then the cokernel relation of $x_{7}$ and $\mathrm{data}$ is a relation of $A$.

Module.Presentation.cokernelSolutiondefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the cokernel solution of x7 and data (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $\mathrm{data}$ be a cokernel data of $f$ and $x_{9}$. Then the cokernel solution of $x_{7}$ and $\mathrm{data}$ is a solution of the cokernel relation of $x_{7}$ and $\mathrm{data}$ and the set of quotients of $x_{2}$ and the range of $f$.

Module.Presentation.cokernelSolution.isPresentationCoredefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

no wording

English

Let $x_{7}$ be a presentation of $A$ and $x_{2}$. Let $\mathrm{data}$ be a cokernel data of $f$ and $x_{9}$. Assume that the span of $A$ and the range of $x_{9}$ is equal to the top. Then $\operatorname{isPresentationCore}$ applied to $x_{7}$, $\mathrm{data}$ and $h$ is an element of $\operatorname{IsPresentationCore}$ applied to the cokernel solution of $x_{7}$ and $\mathrm{data}$.

Module.Presentation.ofExactdefMathlib.Algebra.Module.Presentation.Cokernel, function or constant

Wording

the presentation of x10 and data (from the name)

English

Let $x_{10}$ be a presentation of $A$ and $x_{2}$. Let $\mathrm{data}$ be a cokernel data of $f$ and $x_{12}$. Assume that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $f$ and $\operatorname{coe}$ applied to $g$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $g$. Assume that the span of $A$ and the range of $x_{12}$ is equal to the top. Then the presentation of $x_{10}$ and $\mathrm{data}$ is a presentation of $A$ and $x_{3}$ defined as the presentation of the cokernel of $x_{10}$ and $\mathrm{data}$ and the linear equivalence of $\mathrm{hfg}$ and $\mathrm{hg}$.

Mathlib.Algebra.Module.Presentation.Differentials

Algebra.Presentation.differentialsdefMathlib.Algebra.Module.Presentation.Differentials, function or constant

Wording

the differential of pres (from the name)

English

Let $\mathrm{pres}$ be a presentation of $x$ and $x_{1}$. Then the differential of $\mathrm{pres}$ is a presentation of $S$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

Algebra.Presentation.differentials.hom₁defMathlib.Algebra.Module.Presentation.Differentials, function or constant

Wording

the homomorphism of pres (from the name)

English

Let $\mathrm{pres}$ be a presentation of $x$ and $x_{1}$. Then the homomorphism of $\mathrm{pres}$ is a linear map of $\FinsuppMACRoQ {x_{1}}{S}$ and $\operatorname{Cotangent}$ applied to the extension of $\operatorname{toGenerators}$ applied to $\mathrm{pres}$ defined as the linear combination of $S$ and the function that maps $r$ to $\operatorname{mk}$ applied to the assignment of $\mathrm{pres}$ and $r$.

Algebra.Presentation.differentialsRelationsdefMathlib.Algebra.Module.Presentation.Differentials, function or constant

Wording

the differential relation of pres (from the name)

English

Let $\mathrm{pres}$ be a presentation of $x$ and $x_{1}$. Then the differential relation of $\mathrm{pres}$ is a relation of $S$.

Algebra.Presentation.differentialsSolutiondefMathlib.Algebra.Module.Presentation.Differentials, function or constant

Wording

the differential solution of pres (from the name)

English

Let $\mathrm{pres}$ be a presentation of $x$ and $x_{1}$. Then the differential solution of $\mathrm{pres}$ is a solution of the differential relation of $\mathrm{pres}$ and $\mathrm{KaehlerDifferential}$ applied to $R$ and $S$.

Mathlib.Algebra.Module.Presentation.DirectSum

Module.Presentation.directSumdefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

the direct sum of pres (from the name)

English

Let $\mathrm{pres}$ be a function from elements $i_{1}$ of $x_{1}$ to presentations of $A$ and $M$ applied to $i_{1}$. Then the direct sum of $i_{1}$ is a presentation of $A$ and the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$.

Module.Presentation.finsuppdefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

the finitely supported function of pres and x3 (from the name)

English

Let $\mathrm{pres}$ be a presentation of $A$ and $N$. Let $x_{3}$ be a set. Then the finitely supported function of $\mathrm{pres}$ and $x_{3}$ is a presentation of $A$ and $\FinsuppMACRoQ {x_{3}}{N}$ defined as the presentation of the direct sum of the function that maps $x_{6}$ to $\mathrm{pres}$ and the inverse of the finitely supported function linear equivalence finitely supported function of $A$.

Module.Relations.Solution.IsPresentation.directSum.isRepresentationCoredefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

no wording

English

Assume that for all elements $i$ of $x_{1}$, $\mathrm{solution}$ applied to $i$ is a presentation. Then $\operatorname{isRepresentationCore}$ applied to $h$ is an element of $\operatorname{IsPresentationCore}$ applied to the direct sum of $\mathrm{solution}$.

Module.Relations.Solution.directSumdefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

the direct sum of solution (from the name)

English

Let $\mathrm{solution}$ be a function from elements $i_{1}$ of $x_{1}$ to solutions of $\mathrm{relations}$ applied to $i_{1}$ and $M$ applied to $i_{1}$. Then the direct sum of $i_{1}$ is a solution of the direct sum of $\mathrm{relations}$ and the set of direct sums of $x_{1}$ and the function that maps $i$ to $M$ applied to $i$ defined as the function that maps $\mathrm{solution}$ to $\operatorname{symm}$ applied to the direct sum equivalence, the function that maps $i_{6}$ to the postcomposition of $i_{1}$ applied to $i_{6}$ and $\operatorname{lof}$ applied to $A$, $x_{1}$, $M$ and $i_{6}$ and $\mathrm{solution}$.

Module.Relations.Solution.directSumEquivdefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

the direct sum equivalence (from the name)

English

The direct sum equivalence is an equivalence from the set of solutions of the direct sum of $\mathrm{relations}$ and $N$ to the set of functions from elements $i$ of $x_{1}$ to solutions of $\mathrm{relations}$ applied to $i$ and $N$.

Module.Relations.directSumdefMathlib.Algebra.Module.Presentation.DirectSum, function or constant

Wording

the direct sum of relations (from the name)

English

Let $\mathrm{relations}$ be a function from elements of $x_{1}$ to relations of $A$. Then the direct sum of $\mathrm{relations}$ is a relation of $A$.

Mathlib.Algebra.Module.Presentation.Free

Module.Relations.solutionFinsuppdefMathlib.Algebra.Module.Presentation.Free, function or constant

Wording

the solution finitely supported function of relations (from the name)

English

Let $\mathrm{relations}$ be a relation of $A$. Then the solution finitely supported function of $\mathrm{relations}$ is a solution of $\mathrm{relations}$ and $\FinsuppMACRoQ {\operatorname{G} (\mathrm{relations})}{A}$.

Module.Relations.solutionFinsupp.isPresentationCoredefMathlib.Algebra.Module.Presentation.Free, function or constant

Wording

no wording

English

Let $\mathrm{relations}$ be a relation of $A$. Then $\operatorname{isPresentationCore}$ applied to $\mathrm{relations}$ is an element of $\operatorname{IsPresentationCore}$ applied to the solution finitely supported function of $\mathrm{relations}$.

Module.presentationFinsuppdefMathlib.Algebra.Module.Presentation.Free, function or constant

Wording

the presentation finitely supported function of A and G (from the name)

English

Let $A$ and $G$ be sets. Then the presentation finitely supported function of $A$ and $G$ is a presentation of $A$ and $\FinsuppMACRoQ {G}{A}$.

Mathlib.Algebra.Module.Presentation.RestrictScalars

Module.Presentation.RestrictScalarsDatadefMathlib.Algebra.Module.Presentation.RestrictScalars, type

Wording

no wording

English

Let $\mathrm{presM}$ be a presentation of $B$ and $M$. Let $\mathrm{presB}$ be a presentation of $A$ and $B$. Then the elements of $\operatorname{RestrictScalarsData}$ applied to $\mathrm{presM}$ and $\mathrm{presB}$ are a basic type.

Module.Presentation.restrictScalarsdefMathlib.Algebra.Module.Presentation.RestrictScalars, function or constant

Wording

no wording

English

Let $\mathrm{presM}$ be a presentation of $B$ and $M$. Let $\mathrm{presB}$ be a presentation of $A$ and $B$. Let $\mathrm{data}$ be an element of $\operatorname{RestrictScalarsData}$ applied to $\mathrm{presM}$ and $\mathrm{presB}$. Then $\operatorname{restrictScalars}$ applied to $\mathrm{presM}$, $\mathrm{presB}$ and $\mathrm{data}$ is a presentation of $A$ and $M$.

Mathlib.Algebra.Module.Presentation.Tautological

Module.Presentation.tautologicaldefMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

no wording

English

Let $A$ and $M$ be sets. Then $\operatorname{tautological}$ applied to $A$ and $M$ is a presentation of $A$ and $M$ defined as the presentation of $\mathrm{Module\_\_Presentation\_\_tautologicalSolution\_isPresentation}$ applied to $A$ and $M$.

Module.Presentation.tautological.RinductiveMathlib.Algebra.Module.Presentation.Tautological, type

Wording

no wording

English

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

Module.Presentation.tautological.R.addconstructorMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

the sum of x and x1 (from the name)

English

Let $x$ and $x_{1}$ be elements of $M$. Then the sum of $x$ and $x_{1}$ is an element of $\operatorname{R}$ applied to $A$ and $M$.

Module.Presentation.tautological.R.ctorElimTypedefMathlib.Algebra.Module.Presentation.Tautological, 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 elements $x$ of $M$ and elements $x_{1}$ of $M$ to elements of $\mathrm{motive}$ applied to the sum of $x$ and $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $a$ of $A$ and elements $m$ of $M$ to elements of $\mathrm{motive}$ applied to the scalar multiple of $a$ and $m$.

Module.Presentation.tautological.R.smulconstructorMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

the scalar multiple of a and m (from the name)

English

Let $a$ be an element of $A$. Let $m$ be an element of $M$. Then the scalar multiple of $a$ and $m$ is an element of $\operatorname{R}$ applied to $A$ and $M$.

Module.Presentation.tautologicalRelationsdefMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

the tautological relation of A and M (from the name)

English

Let $A$ and $M$ be sets. Then the tautological relation of $A$ and $M$ is a relation of $A$.

Module.Presentation.tautologicalRelationsSolutionEquivdefMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

the tautological relation solution equivalence (from the name)

English

The tautological relation solution equivalence is an equivalence from the set of solutions of the tautological relation of $A$ and $M$ and $N$ to the set of linear maps of $M$ and $N$.

Module.Presentation.tautologicalSolutiondefMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

the tautological solution of A and M (from the name)

English

Let $A$ and $M$ be sets. Then the tautological solution of $A$ and $M$ is a solution of the tautological relation of $A$ and $M$ and $M$ defined as $\operatorname{symm}$ applied to the tautological relation solution equivalence and the identity.

Module.Presentation.tautologicalSolutionIsPresentationCoredefMathlib.Algebra.Module.Presentation.Tautological, function or constant

Wording

no wording

English

Let $A$ and $M$ be sets. Then $\operatorname{tautologicalSolutionIsPresentationCore}$ applied to $A$ and $M$ is an element of $\operatorname{IsPresentationCore}$ applied to the tautological solution of $A$ and $M$.

Mathlib.Algebra.Module.Presentation.Tensor

Module.Presentation.tensordefMathlib.Algebra.Module.Presentation.Tensor, function or constant

Wording

the tensor of x7 and x8 (from the name)

English

Let $x_{7}$ be a presentation of $A$ and $x_{1}$. Let $x_{8}$ be a presentation of $A$ and $x_{2}$. Then the tensor of $x_{7}$ and $x_{8}$ is a presentation of $A$ and the set of tensor products of $x_{1}$ and $x_{2}$.

Module.Relations.Solution.isPresentationCoreTensordefMathlib.Algebra.Module.Presentation.Tensor, function or constant

Wording

no wording

English

Assume that $x_{9}$ is a presentation. Assume that $x_{10}$ is a presentation. Then $\operatorname{isPresentationCoreTensor}$ applied to $h$ and $h_{1}$ is an element of $\operatorname{IsPresentationCore}$ applied to the tensor of $x_{9}$ and $x_{10}$.

Module.Relations.Solution.tensordefMathlib.Algebra.Module.Presentation.Tensor, function or constant

Wording

the tensor of x9 and x10 (from the name)

English

Let $x_{9}$ be a solution of $x_{7}$ and $x_{1}$. Let $x_{10}$ be a solution of $x_{8}$ and $x_{2}$. Then the tensor of $x_{9}$ and $x_{10}$ is a solution of the tensor of $x_{7}$ and $x_{8}$ and the set of tensor products of $x_{1}$ and $x_{2}$.

Module.Relations.tensordefMathlib.Algebra.Module.Presentation.Tensor, function or constant

Wording

the tensor of x1 and x2 (from the name)

English

Let $x_{1}$ and $x_{2}$ be relations of $A$. Then the tensor of $x_{1}$ and $x_{2}$ is a relation of $A$.

Mathlib.Algebra.Module.Projective

Module.ProjectiveclassMathlib.Algebra.Module.Projective, predicate

Wording

R is projective (from the docstring)

English

Let $R$ and $P$ be sets. Then we can say that $R$ is projective.

Mathlib.Algebra.Module.RingHom

RingHom.smulOneHomdefMathlib.Algebra.Module.RingHom, function or constant

Wording

the scalar multiple one homomorphism (from the name)

English

The scalar multiple one homomorphism is a ring homomorphism of $R$ and $S$.

ringHomEquivModuleIsScalarTowerdefMathlib.Algebra.Module.RingHom, function or constant

Wording

no wording

English

$\mathrm{ringHomEquivModuleIsScalarTower}$ is an equivalence from the set of ring homomorphisms of $R$ and $S$ to $\SubtypeSet {\mathrm{\_inst}}{\mathrm{IsScalarTower} (R , S , S)}$.

Mathlib.Algebra.Module.Shrink

Shrink.linearEquivdefMathlib.Algebra.Module.Shrink, function or constant

Wording

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

English

Let $R$ and $x$ be sets. Then the linear equivalence of $R$ and $x$ is a linear equivalence of the set of shrinks of $x$ and $x$ defined as the linear equivalence of $R$ and the additive equivalence.

Mathlib.Algebra.Module.SnakeLemma

SnakeLemma.δdefMathlib.Algebra.Module.SnakeLemma, function or constant

Wording

no wording

English

Let $x_{19}$ be a linear map of $x_{1}$ and $x_{4}$. Let $x_{20}$ be a linear map of $x_{2}$ and $x_{5}$. Let $x_{21}$ be a linear map of $x_{3}$ and $x_{6}$. Let $x_{22}$ be a linear map of $x_{1}$ and $x_{2}$. Let $x_{23}$ be a linear map of $x_{2}$ and $x_{3}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{22}$ and $\operatorname{coe}$ applied to $x_{23}$. Let $x_{24}$ be a linear map of $x_{4}$ and $x_{5}$. Let $x_{25}$ be a linear map of $x_{5}$ and $x_{6}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{24}$ and $\operatorname{coe}$ applied to $x_{25}$. Assume that the composition of $x_{24}$ and $x_{19}$ is equal to the composition of $x_{20}$ and $x_{22}$. Assume that the composition of $x_{25}$ and $x_{20}$ is equal to the composition of $x_{21}$ and $x_{23}$. Let $x_{26}$ be a function from elements of $x_{3}$ to elements of $x_{2}$ such that $\operatorname{comp}$ applied to $\operatorname{coe}$ applied to $x_{23}$ and $x_{26}$ is equal to $\mathrm{id}$. Let $x_{27}$ be a function from elements of $x_{5}$ to elements of $x_{4}$ such that $\operatorname{comp}$ applied to $x_{27}$ and $\operatorname{coe}$ applied to $x_{24}$ is equal to $\mathrm{id}$. Let $x_{34}$ be a linear map of $x_{28}$ and $x_{3}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{34}$ and $\operatorname{coe}$ applied to $x_{21}$. Let $x_{35}$ be a linear map of $x_{4}$ and $x_{29}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{19}$ and $\operatorname{coe}$ applied to $x_{35}$. Then $\mathrm{SnakeLemma\_\_\_u3b4\_}$ applied to $x_{19}$, $x_{20}$, $x_{21}$, $x_{22}$, $x_{23}$, $\mathrm{hf}$, $x_{24}$, $x_{25}$, $\mathrm{hg}$, $h$, $h_{1}$, $x_{26}$, $h_{2}$, $x_{27}$, $h_{3}$, $x_{34}$, $h_{4}$, $x_{35}$ and $h_{5}$ is a linear map of $x_{28}$ and $x_{29}$.

SnakeLemma.δ'defMathlib.Algebra.Module.SnakeLemma, function or constant

Wording

no wording

English

Let $x_{19}$ be a linear map of $x_{1}$ and $x_{4}$. Let $x_{20}$ be a linear map of $x_{2}$ and $x_{5}$. Let $x_{21}$ be a linear map of $x_{3}$ and $x_{6}$. Let $x_{22}$ be a linear map of $x_{1}$ and $x_{2}$. Let $x_{23}$ be a linear map of $x_{2}$ and $x_{3}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{22}$ and $\operatorname{coe}$ applied to $x_{23}$. Let $x_{24}$ be a linear map of $x_{4}$ and $x_{5}$. Let $x_{25}$ be a linear map of $x_{5}$ and $x_{6}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{24}$ and $\operatorname{coe}$ applied to $x_{25}$. Assume that the composition of $x_{24}$ and $x_{19}$ is equal to the composition of $x_{20}$ and $x_{22}$. Assume that the composition of $x_{25}$ and $x_{20}$ is equal to the composition of $x_{21}$ and $x_{23}$. Let $x_{32}$ be a linear map of $x_{26}$ and $x_{3}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{32}$ and $\operatorname{coe}$ applied to $x_{21}$. Let $x_{33}$ be a linear map of $x_{4}$ and $x_{27}$ such that $\operatorname{Exact}$ holds for $\operatorname{coe}$ applied to $x_{19}$ and $\operatorname{coe}$ applied to $x_{33}$. Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $x_{23}$. Assume that $\operatorname{coe}$ applied to $x_{24}$ is injective. Then $\mathrm{SnakeLemma\_\_\_u3b4\_'}$ applied to $x_{19}$, $x_{20}$, $x_{21}$, $x_{22}$, $x_{23}$, $\mathrm{hf}$, $x_{24}$, $x_{25}$, $\mathrm{hg}$, $h$, $h_{1}$, $x_{32}$, $h_{2}$, $x_{33}$, $h_{3}$, $h_{4}$ and $h_{5}$ is a linear map of $x_{26}$ and $x_{27}$.

Mathlib.Algebra.Module.SpanRank

Submodule.generatorsdefMathlib.Algebra.Module.SpanRank, function or constant

Wording

the generator of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the generator of $p$ is an element of $\wp M$ defined as $\operatorname{choose}$ applied to $\mathrm{Submodule\_\_exists\_span\_set\_card\_eq\_spanRank}$ applied to $p$.

Submodule.spanFinrankdefMathlib.Algebra.Module.SpanRank, function or constant

Wording

the span finite rank of p (from the name)

English

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

Submodule.spanRankdefMathlib.Algebra.Module.SpanRank, function or constant

Wording

the span rank of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the span rank of $p$ is a cardinal defined as the infimum of the function that maps $s$ to $\operatorname{mk}$ applied to the set of elements of $s$.

Mathlib.Algebra.Module.StablyFree.Basic

Module.IsStablyFreeclassMathlib.Algebra.Module.StablyFree.Basic, predicate

Wording

M is stably free with respect to R (from the name)

English

generation took over the time limit

Mathlib.Algebra.Module.Submodule.Basic

SubspacedefMathlib.Algebra.Module.Submodule.Basic, type

Wording

subspace of R and M (from the name)

English

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

Mathlib.Algebra.Module.Submodule.Bilinear

Submodule.map₂defMathlib.Algebra.Module.Submodule.Bilinear, function or constant

Wording

the map of p and q (from the name)

English

Let $f$ be a linear map of $M$ and the set of linear maps of $N$ and $P$. Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $R$ and $N$. Then the map of $p$ and $q$ is a submodule of $R$ and $P$ defined as the supremum of the function that maps $s$ to the map of $f$ applied to $s$ and $q$.

Mathlib.Algebra.Module.Submodule.Defs

SubmodulestructureMathlib.Algebra.Module.Submodule.Defs, type

Wording

submodule of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the submodules of $R$ and $M$ are a basic type.

Submodule.copydefMathlib.Algebra.Module.Submodule.Defs, function or constant

Wording

the copy of p and s (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Let $s$ be an element of $\wp M$ such that $\EqtMACRoH {s}{p}$. Then the copy of $p$ and $s$ is a submodule of $R$ and $M$.

Submodule.ofClassdefMathlib.Algebra.Module.Submodule.Defs, function or constant

Wording

the submodule of s (from the name)

English

Let $s$ be an element of $S$. Then the submodule of $s$ is a submodule of $R$ and $M$.

Submodule.ofLinearCombdefMathlib.Algebra.Module.Submodule.Defs, function or constant

Wording

the submodule of C (from the name)

English

Let $C$ be an element of $\wp M$ such that $C$ is nonempty and for all elements $x_{3}$ of $M$, if $x_{3}$ is an element of $C$, then for all elements $y$ of $M$, if $y$ is an element of $C$, then for all elements $a$ of $R$, for all elements $b$ of $R$, $\HSMulhSMulMACRoAL {a}{x_{3}}+ \HSMulhSMulMACRoAL {b}{y}$ is an element of $C$. Then the submodule of $C$ is a submodule of $R$ and $M$.

Submodule.toAddSubgroupdefMathlib.Algebra.Module.Submodule.Defs, function or constant

Wording

the additive subgroup of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the additive subgroup of $p$ is an additive subgroup of $M$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddSubmonoid}$ applied to $p$ and the function that maps $x_{2}$ to $\mathrm{Submodule\_\_neg\_mem}$ applied to $p$.

Submodule.toSubMulActiondefMathlib.Algebra.Module.Submodule.Defs, function or constant

Wording

the difference multiplicative action of self (from the name)

English

Let $\mathrm{self}$ be a submodule of $R$ and $M$. Then the difference multiplicative action of $\mathrm{self}$ is a difference multiplicative action of $R$ and $M$ defined as $\operatorname{mk}$ applied to the carrier of $\operatorname{toAddSubsemigroup}$ applied to $\operatorname{toAddSubmonoid}$ applied to $\mathrm{self}$ and $\mathrm{Submodule\_\_smul\_mem'}$ applied to $\mathrm{self}$.

Mathlib.Algebra.Module.Submodule.EqLocus

LinearMap.eqLocusdefMathlib.Algebra.Module.Submodule.EqLocus, function or constant

Wording

no wording

English

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

Mathlib.Algebra.Module.Submodule.Equiv

LinearEquiv.ofBijectivedefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of f and hf (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the linear equivalence of $f$ and $\mathrm{hf}$ is a linear equivalence of $M$ and $x_{1}$.

LinearEquiv.ofEqdefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$ such that $\EqtMACRoH {p}{q}$. Then the linear equivalence of $p$ and $q$ is a linear equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {q}{x_{3}})}$.

LinearEquiv.ofInjectivedefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of f and h2 (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the linear equivalence of $f$ and $h_{2}$ is a linear equivalence of $M$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{9}})}$.

LinearEquiv.ofLeftInversedefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of h2 (from the name)

English

Assume that $\operatorname{LeftInverse}$ holds for $g$ and $\operatorname{coe}$ applied to $f$. Then the linear equivalence of $h_{2}$ is a linear equivalence of $M$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{9}})}$.

LinearEquiv.ofSubmodule'defMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of f and U (from the name)

English

Let $f$ be a linear equivalence of $M$ and $x_{1}$. Let $U$ be a submodule of $x$ and $x_{1}$. Then the linear equivalence of $f$ and $U$ is a linear equivalence of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{comap} (\operatorname{toLinearMap} (f), U)}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {U}{x_{11}})}$.

LinearEquiv.ofSubmodulesdefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of p and q (from the name)

English

Let $e$ be a linear equivalence of $M$ and $x_{1}$. Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $x$ and $x_{1}$ such that the map of $\operatorname{toLinearMap}$ applied to $e$ and $p$ is equal to $q$. Then the linear equivalence of $p$ and $q$ is a linear equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {q}{x_{10}})}$ defined as the composition of the submodule map of $e$ and $p$ and the linear equivalence of the map of $\operatorname{toLinearMap}$ applied to $e$ and $p$ and $q$.

LinearEquiv.ofTopdefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the linear equivalence of p and h (from the name)

English

Let $p$ be a submodule of $R$ and $M$ such that $p$ is equal to the top. Then the linear equivalence of $p$ and $h$ is a linear equivalence of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$ and $M$.

LinearMap.codRestrictOfInjectivedefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

no wording

English

Let $f$ be a linear map of $x$ and $x_{1}$. Let $i$ be a linear map of $x_{2}$ and $x_{1}$ such that $\operatorname{coe}$ applied to $i$ is injective and for all elements $x_{10}$ of $x$, $f$ applied to $x_{10}$ is an element of the range of $i$. Then $\operatorname{codRestrictOfInjective}$ applied to $f$, $i$, $\mathrm{hi}$ and $\mathrm{hf}$ is a linear map of $x$ and $x_{2}$ defined as the composition of $\operatorname{toLinearMap}$ applied to the inverse of the linear equivalence of $i$ and $\mathrm{hi}$ and $\operatorname{codRestrict}$ applied to the range of $i$, $f$ and $\mathrm{hf}$.

LinearMap.codRestrict₂defMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

no wording

English

Let $f$ be a linear map of $x$ and the set of linear maps of $x_{1}$ and $M$. Let $i$ be a linear map of $x_{2}$ and $M$ such that $\operatorname{coe}$ applied to $i$ is injective and for all elements $x_{12}$ of $x$, for all elements $y$ of $x_{1}$, $\operatorname{coe}$ applied to $f$, $x_{12}$ and $y$ is an element of the range of $i$. Then $\mathrm{LinearMap\_\_codRestrict\_u2082\_}$ applied to $f$, $i$, $\mathrm{hi}$ and $\mathrm{hf}$ is a linear map of $x$ and the set of linear maps of $x_{1}$ and $x_{2}$.

Submodule.comap_equiv_self_of_inj_of_ledefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the preimage equivalence self of hf and h (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Assume that $p \leq \operatorname{range} (f)$. Then the preimage equivalence self of $\mathrm{hf}$ and $h$ is a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{comap} (f , p)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$.

Submodule.equivSubtypeMapdefMathlib.Algebra.Module.Submodule.Equiv, function or constant

Wording

the equivalence subtype map of p and q (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Let $q$ be a submodule of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {p}{x_{5}})}$. Then the equivalence subtype map of $p$ and $q$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {q}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{subtype} (p), q)}{x_{4}})}$.

Mathlib.Algebra.Module.Submodule.Invariant

Module.End.invtSubmoduledefMathlib.Algebra.Module.Submodule.Invariant, function or constant

Wording

no wording

English

Let $f$ be an end of $R$ and $M$. Then $\operatorname{invtSubmodule}$ applied to $f$ is a sublattice of the set of submodules of $R$ and $M$.

Mathlib.Algebra.Module.Submodule.IterateMapComap

LinearMap.iterateMapComapdefMathlib.Algebra.Module.Submodule.IterateMapComap, function or constant

Wording

no wording

English

Let $f$ and $i$ be linear maps of $N$ and $M$. Let $n$ be a natural number. Let $x_{5}$ be a submodule of $R$ and $N$. Then $\operatorname{iterateMapComap}$ applied to $f$, $i$, $n$ and $x_{5}$ is a submodule of $R$ and $N$ defined as $\operatorname{iterate}$ applied to the function that maps $K$ to the preimage of $f$ and the map of $i$ and $K$, $n$ and $x_{5}$.

Mathlib.Algebra.Module.Submodule.Ker

LinearMap.iterateKerdefMathlib.Algebra.Module.Submodule.Ker, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $M$. Then $\operatorname{iterateKer}$ applied to $f$ is an order homomorphism of $\Natural$ and the set of submodules of $R$ and $M$.

LinearMap.kerdefMathlib.Algebra.Module.Submodule.Ker, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Then the kernel of $f$ is a submodule of $R$ and $M$ defined as the preimage of $f$ and the bottom.

Mathlib.Algebra.Module.Submodule.Lattice

AddSubgroup.toIntSubmoduledefMathlib.Algebra.Module.Submodule.Lattice, function or constant

Wording

the integer submodule (from the name)

English

The integer submodule is an order isomorphism of the set of additive subgroups of $M$ and the set of submodules of $\Integer$ and $M$.

AddSubmonoid.toNatSubmoduledefMathlib.Algebra.Module.Submodule.Lattice, function or constant

Wording

the natural submodule (from the name)

English

The natural submodule is an order isomorphism of the set of additive submonoids of $M$ and the set of submodules of $\Natural$ and $M$.

Submodule.botEquivPUnitdefMathlib.Algebra.Module.Submodule.Lattice, function or constant

Wording

the bottom submodule (from the docstring)

English

The bottom submodule is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{bot}}{x_{3}})}$ and $\mathrm{PUnit}$.

Submodule.topEquivdefMathlib.Algebra.Module.Submodule.Lattice, function or constant

Wording

the top submodule (from the docstring)

English

The top submodule is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $M$.

Mathlib.Algebra.Module.Submodule.LinearMap

LinearMap.codLiftdefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

the codomain lift of f and p (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $p$ be a linear map of $x_{9}$ and $x_{1}$ such that $\operatorname{coe}$ applied to $p$ is injective and for all elements $c$ of $M$, $f$ applied to $c$ is an element of the range of $\operatorname{coe}$ applied to $p$. Then the codomain lift of $f$ and $p$ is a linear map of $M$ and $x_{9}$.

LinearMap.codRestrictdefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

no wording

English

Let $p$ be a submodule of $x$ and $x_{1}$. Let $f$ be a linear map of $M$ and $x_{1}$ such that for all elements $c$ of $M$, $\MembershipmemMACRoT {p}{f (c)}$. Then $\operatorname{codRestrict}$ applied to $p$, $f$ and $h$ is a linear map of $M$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$.

LinearMap.domRestrictdefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

the restriction of f and p (from the docstring)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $p$ be a submodule of $R$ and $M$. Then the restriction of $f$ and $p$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$ and $x_{1}$ defined as the composition of $f$ and the subtype of $p$.

LinearMap.domRestrict'defMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

no wording

English

Let $p$ be a submodule of $R$ and $M$. Then $\operatorname{domRestrict'}$ applied to $p$ is a linear map of the set of linear maps of $M$ and $x$ and the set of linear maps of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {p}{x_{6}})}$ and $x$.

LinearMap.restrictdefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $x_{1}$ such that for all elements $x_{11}$ of $M$, if $x_{11}$ is an element of $p$, then $\MembershipmemMACRoT {q}{f (x_{11})}$. Then $\operatorname{restrict}$ applied to $f$ and $\mathrm{hf}$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {q}{x_{10}})}$.

SMulMemClass.subtypedefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

the subtype of #1 (from the name)

English

Let $\mathrm{S'}$ be an element of $A$. Then the subtype of $\mathrm{S'}$ is a linear map of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{S'}}{x_{4}})}$ and $M$.

Submodule.inclusiondefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $p \leq \mathrm{p'}$. Then the inclusion of $h$ is a linear map of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{p'}}{x_{4}})}$.

Submodule.subtypedefMathlib.Algebra.Module.Submodule.LinearMap, function or constant

Wording

the subtype of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the subtype of $p$ is a linear map of $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {p}{x_{2}})}$ and $M$.

Mathlib.Algebra.Module.Submodule.Map

LinearEquiv.submoduleMapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the submodule map of e and p (from the name)

English

Let $e$ be a linear equivalence of $M$ and $x_{1}$. Let $p$ be a submodule of $R$ and $M$. Then the submodule map of $e$ and $p$ is a linear equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toLinearMap} (e), p)}{x_{10}})}$.

LinearMap.submoduleComapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the submodule preimage of f and q (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $q$ be a submodule of $x$ and $x_{1}$. Then the submodule preimage of $f$ and $q$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{comap} (f , q)}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {q}{x_{10}})}$.

LinearMap.submoduleMapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the submodule map of f and p (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $p$ be a submodule of $R$ and $M$. Then the submodule map of $f$ and $p$ is a linear map of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {p}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{map} (f , p)}{x_{10}})}$.

Submodule.comapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the preimage of f and p (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $p$ be a submodule of $x$ and $x_{1}$. Then the preimage of $f$ and $p$ is a submodule of $R$ and $M$.

Submodule.comapSubtypeEquivOfLedefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the preimage subtype equivalence of hpq (from the name)

English

Assume that $p \leq q$. Then the preimage subtype equivalence of $\mathrm{hpq}$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{comap} (\operatorname{subtype} (q), p)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$.

Submodule.compatibleMapsdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the compatible map of x6 and x7 (from the name)

English

Let $x_{6}$ be a submodule of $S$ and $N$. Let $x_{7}$ be a submodule of $S$ and $x$. Then the compatible map of $x_{6}$ and $x_{7}$ is a submodule of $S$ and the set of linear maps of $N$ and $x$.

Submodule.equivMapOfInjectivedefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the equivalence map of f and p (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is injective. Let $p$ be a submodule of $R$ and $M$. Then the equivalence map of $f$ and $p$ is a linear equivalence of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {p}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{map} (f , p)}{x_{11}})}$.

Submodule.gciMapComapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

no wording

English

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

Submodule.giMapComapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

no wording

English

Assume that $\operatorname{Surjective}$ holds for $\operatorname{coe}$ applied to $f$. Then $\operatorname{giMapComap}$ applied to $\mathrm{hf}$ is a Galois insertion of $\operatorname{map}$ applied to $f$ and $\operatorname{comap}$ applied to $f$.

Submodule.mapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the map of f and p (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Let $p$ be a submodule of $R$ and $M$. Then the map of $f$ and $p$ is a submodule of $x$ and $x_{1}$.

Submodule.orderIsoMapComapdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the order isomorphism map preimage of f (from the name)

English

Let $f$ be a linear equivalence of $M$ and $x_{1}$. Then the order isomorphism map preimage of $f$ is an order isomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $x$ and $x_{1}$ defined as the order isomorphism map preimage of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{bijective}$ applied to $f$.

Submodule.orderIsoMapComapOfBijectivedefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the order isomorphism map preimage of f and hf (from the name)

English

Let $f$ be a linear map of $M$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the order isomorphism map preimage of $f$ and $\mathrm{hf}$ is an order isomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $x$ and $x_{1}$.

Submodule.submoduleOfdefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the submodule of p and q (from the name)

English

Let $p$ and $q$ be submodules of $R$ and $M$. Then the submodule of $p$ and $q$ is a submodule of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {q}{x_{3}})}$ defined as the preimage of the subtype of $q$ and $p$.

Submodule.submoduleOfEquivOfLedefMathlib.Algebra.Module.Submodule.Map, function or constant

Wording

the submodule of h (from the name)

English

Assume that $p \leq q$. Then the submodule of $h$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{submoduleOf} (p , q)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {p}{x_{4}})}$.

Mathlib.Algebra.Module.Submodule.Pointwise

Submodule.negOrderIsodefMathlib.Algebra.Module.Submodule.Pointwise, function or constant

Wording

the negation order isomorphism (from the name)

English

The negation order isomorphism is an order isomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $R$ and $M$ defined as $\operatorname{mk}$ applied to the negation of the set of submodules of $R$ and $M$ and $\mathrm{Submodule\_\_neg\_le\_neg}$.

Mathlib.Algebra.Module.Submodule.Range

LinearMap.iterateRangedefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $M$. Then $\operatorname{iterateRange}$ applied to $f$ is an order homomorphism of $\Natural$ and the set of order duals of the set of submodules of $R$ and $M$.

LinearMap.rangedefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a linear map of $M$ and $x_{1}$. Then the range of $f$ is a submodule of $x$ and $x_{1}$.

LinearMap.rangeRestrictdefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

no wording

English

Let $f$ be a linear map of $M$ and $x_{1}$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a linear map of $M$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{9}})}$ defined as $\operatorname{codRestrict}$ applied to the range of $f$, $f$ and $\mathrm{LinearMap\_\_mem\_range\_self}$ applied to $f$.

LinearMap.submoduleImagedefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

the submodule image of x5 and N (from the name)

English

Let $x_{5}$ be a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {O}{x_{6}})}$ and $\mathrm{M'}$. Let $N$ be a submodule of $R$ and $M$. Then the submodule image of $x_{5}$ and $N$ is a submodule of $R$ and $\mathrm{M'}$ defined as the map of $x_{5}$ and the preimage of the subtype of $O$ and $N$.

Submodule.MapSubtype.orderEmbeddingdefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

the order embedding of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the order embedding of $p$ is an order embedding of the set of submodules of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and the set of submodules of $R$ and $M$ defined as the composition of the relation embedding of the order isomorphism of $p$ and the induced relation of the function that maps $p_{1}$ and $\mathrm{p'}$ to $\mathrm{Leq} (p_{1} , \mathrm{p'})$ and the function that maps $\mathrm{p'1}$ to $\mathrm{Leq} (\mathrm{p'1} , p)$.

Submodule.MapSubtype.orderIsodefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

the order isomorphism of p (from the name)

English

Let $p$ be a submodule of $R$ and $M$. Then the order isomorphism of $p$ is an order isomorphism of the set of submodules of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and $\SubtypeSet {\mathrm{p'}}{\mathrm{Leq} (\mathrm{p'} , p)}$.

Submodule.mapIicdefMathlib.Algebra.Module.Submodule.Range, function or constant

Wording

no wording

English

Let $p$ be a submodule of $R$ and $M$. Then $\operatorname{mapIic}$ applied to $p$ is an order isomorphism of the set of submodules of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {p}{x_{3}})}$ and the set of elements of $\operatorname{Iic}$ applied to $p$ defined as the order isomorphism of $p$.

Mathlib.Algebra.Module.Submodule.RestrictScalars

Submodule.restrictScalarsdefMathlib.Algebra.Module.Submodule.RestrictScalars, function or constant

Wording

no wording

English

Let $S$ be a set. Let $V$ be a submodule of $R$ and $M$. Then $\operatorname{restrictScalars}$ applied to $S$ and $V$ is a submodule of $S$ and $M$.

Submodule.restrictScalarsEmbeddingdefMathlib.Algebra.Module.Submodule.RestrictScalars, function or constant

Wording

no wording

English

Let $S$, $R$ and $M$ be sets. Then $\operatorname{restrictScalarsEmbedding}$ applied to $S$, $R$ and $M$ is an order embedding of the set of submodules of $R$ and $M$ and the set of submodules of $S$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $S$ and $\mathrm{Submodule\_\_restrictScalars\_injective}$ applied to $S$, $R$ and $M$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{Submodule\_\_restrictScalars\_le}$ applied to $S$.

Submodule.restrictScalarsEquivdefMathlib.Algebra.Module.Submodule.RestrictScalars, function or constant

Wording

no wording

English

Let $S$, $R$ and $M$ be sets. Let $p$ be a submodule of $R$ and $M$. Then $\operatorname{restrictScalarsEquiv}$ applied to $S$, $R$, $M$ and $p$ is a linear equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{restrictScalars} (S , p)}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {p}{x_{7}})}$.

Submodule.restrictScalarsLatticeHomdefMathlib.Algebra.Module.Submodule.RestrictScalars, function or constant

Wording

no wording

English

Let $S$, $R$ and $M$ be sets. Then $\operatorname{restrictScalarsLatticeHom}$ applied to $S$, $R$ and $M$ is a complete lattice homomorphism of the set of submodules of $R$ and $M$ and the set of submodules of $S$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $S$ and $\mathrm{Submodule\_\_restrictScalars\_sInf}$ applied to $S$ and $\mathrm{Submodule\_\_restrictScalars\_sSup}$ applied to $S$.

Mathlib.Algebra.Module.Torsion.Basic

AddSubgroup.torsionBydefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

no wording

English

Let $A$ be a set. Let $n$ be an integer. Then $\operatorname{torsionBy}$ applied to $A$ and $n$ is an additive subgroup of $A$ defined as the additive subgroup of $\operatorname{torsionBy}$ applied to $\Integer$, $A$ and $n$.

AddSubgroup.torsionByStxdefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

no wording

English

generation took over the time limit

Ideal.quotTorsionOfEquivSpanSingletondefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the span of R (from the docstring)

English

Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $M$. Then the span of $R$ is a linear equivalence of the set of quotients of $R$ and the torsion of $x_{3}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{span} (R , \operatorname{singleton} (x_{3}))}{x_{4}})}$.

Ideal.torsionOfdefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the torsion of x3 (from the name)

English

Let $R$ and $M$ be sets. Let $x_{3}$ be an element of $M$. Then the torsion of $x_{3}$ is an ideal of $R$ defined as the kernel of the span singleton of $x_{3}$.

Module.IsTorsiondefMathlib.Algebra.Module.Torsion.Basic, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Then $\operatorname{IsTorsion}$ holds for $R$ and $M$, if for all elements $x_{3}$ of $M$, there exists an element $a$ of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (R)}{x_{4}})}$, such that $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{3}}}{0}$.

Module.IsTorsion'defMathlib.Algebra.Module.Torsion.Basic, predicate

Wording

M is a torsion with respect to S (from the name)

English

Let $M$ and $S$ be sets. Then $M$ is a torsion with respect to $S$, if for all elements $x_{2}$ of $M$, there exists an element $a$ of $S$, such that $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{2}}}{0}$.

Module.IsTorsionBydefMathlib.Algebra.Module.Torsion.Basic, predicate

Wording

no wording

English

Let $R$ and $M$ be sets. Let $a$ be an element of $R$. Then $\operatorname{IsTorsionBy}$ holds for $R$, $M$ and $a$, if for all elements $x_{3}$ of $M$, $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{3}}}{0}$.

Module.IsTorsionBySetdefMathlib.Algebra.Module.Torsion.Basic, predicate

Wording

s is a torsion by set (from the name)

English

Let $R$ and $M$ be sets. Let $s$ be an element of $\wp R$. Then $s$ is a torsion by set, if for all elements $x_{3}$ of $M$, for all elements $a$ of $s$, $\EqtMACRoH {\HSMulhSMulMACRoAL {a}{x_{3}}}{0}$.

Module.IsTorsionBySet.semilinearMapdefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the semilinear map of hM (from the name)

English

Assume that $I$ is a torsion by set. Then the semilinear map of $\mathrm{hM}$ is a linear map of $M$ and $M$.

Submodule.pOrderdefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the order of hM and x3 (from the name)

English

Assume that $M$ is a torsion with respect to $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{powers} (p)}{x_{5}})}$. Let $x_{3}$ be an element of $M$. Then the order of $\mathrm{hM}$ and $x_{3}$ is an element of $\Natural$.

Submodule.submodule_torsionBy_orderIsodefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the submodule torsion by order isomorphism of a (from the name)

English

Let $a$ be an element of $R$. Then the submodule torsion by order isomorphism of $a$ is an order isomorphism of the set of submodules of the set of quotients of $R$ and the span of $R$ and $\operatorname{singleton}$ applied to $a$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{torsionBy} (R , M , a)}{x_{3}})}$ and the set of submodules of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{torsionBy} (R , M , a)}{x_{4}})}$.

Submodule.torsiondefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the torsion of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the torsion of $R$ and $M$ is a submodule of $R$ and $M$ defined as the torsion of $M$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{nonZeroDivisors} (R)}{x_{3}})}$.

Submodule.torsion'defMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the torsion of M and S (from the name)

English

Let $R$, $M$ and $S$ be sets. Then the torsion of $M$ and $S$ is a submodule of $R$ and $M$.

Submodule.torsionBydefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

no wording

English

Let $R$ and $M$ be sets. Let $a$ be an element of $R$. Then $\operatorname{torsionBy}$ applied to $R$, $M$ and $a$ is a submodule of $R$ and $M$ defined as the kernel of the linear map of $a$.

Submodule.torsionBySetdefMathlib.Algebra.Module.Torsion.Basic, function or constant

Wording

the torsion by set of s (from the name)

English

Let $R$ and $M$ be sets. Let $s$ be an element of $\wp R$. Then the torsion by set of $s$ is a submodule of $R$ and $M$ defined as the infimum of the image of $\operatorname{torsionBy}$ applied to $R$ and $M$ and $s$.

Mathlib.Algebra.Module.Torsion.Free

Module.IsTorsionFreeclassMathlib.Algebra.Module.Torsion.Free, predicate

Wording

no wording

English

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

Mathlib.Algebra.Module.Torsion.PrimaryComponent

Ideal.primaryComponentdefMathlib.Algebra.Module.Torsion.PrimaryComponent, function or constant

Wording

the primary component of M and I (from the name)

English

Let $M$ be a set. Let $I$ be an ideal of $A$. Then the primary component of $M$ and $I$ is a submodule of $A$ and $M$ defined as the supremum of the function that maps $i$ to the torsion by set of $I ^ {i}$.

Ideal.primaryComponent.mapdefMathlib.Algebra.Module.Torsion.PrimaryComponent, function or constant

Wording

the map of I and x7 (from the name)

English

Let $I$ be an ideal of $A$. Let $x_{7}$ be a linear map of $x$ and $x_{1}$. Then the map of $I$ and $x_{7}$ is a linear map of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{primaryComponent} (x , I)}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{primaryComponent} (x_{1} , I)}{x_{9}})}$.

Mathlib.Algebra.Module.TransferInstance

AddEquiv.linearEquivdefMathlib.Algebra.Module.TransferInstance, function or constant

Wording

the linear equivalence of R and e (from the name)

English

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

Mathlib.Algebra.Module.ULift

ULift.moduleEquivdefMathlib.Algebra.Module.ULift, function or constant

Wording

the module equivalence (from the name)

English

The module equivalence is a linear equivalence of $\mathrm{ULift}$ applied to $M$ and $M$.

Mathlib.Algebra.Module.ZLattice.Basic

IsZLatticeclassMathlib.Algebra.Module.ZLattice.Basic, predicate

Wording

L is a lattice (from the name)

English

Let $K$ be a set. Let $L$ be a submodule of $\Integer$ and $E$. Then we can say that $L$ is a lattice.

IsZLattice.basisdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the basis of L (from the name)

English

Let $L$ be a submodule of $\Integer$ and the set of functions from elements of $x$ to real numbers. Then the basis of $L$ is a basis of $\Integer$ and $\SubtypeSet {x_{2}}{(\MembershipmemMACRoT {L}{x_{2}})}$.

Module.Basis.ofZLatticeBasisdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the basis of L and b (from the name)

English

Let $K$ be a set. Let $L$ be a submodule of $\Integer$ and $E$. Let $b$ be a basis of $\Integer$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {L}{x_{6}})}$. Then the basis of $L$ and $b$ is a basis of $K$ and $E$.

Module.Basis.ofZLatticeComapdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the basis of K (from the docstring)

English

Let $K$ be a set. Let $L$ be a submodule of $\Integer$ and $E$. Let $e$ be a linear equivalence of $F$ and $E$. Let $b$ be a basis of $\Integer$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {L}{x_{7}})}$. Then the basis of $K$ is a basis of $\Integer$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{comap} (L , \operatorname{toLinearMap} (e))}{x_{6}})}$ defined as the map of $b$ and the preimage equivalence of $L$ and $e$.

ZLattice.comapdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the preimage of L and e (from the name)

English

Let $K$ be a set. Let $L$ be a submodule of $\Integer$ and $E$. Let $e$ be a linear map of $F$ and $E$. Then the preimage of $L$ and $e$ is a submodule of $\Integer$ and $F$ defined as the preimage of $\operatorname{restrictScalars}$ applied to $\Integer$ and $e$ and $L$.

ZLattice.comap_equivdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the preimage equivalence of L and e (from the name)

English

Let $K$ be a set. Let $L$ be a submodule of $\Integer$ and $E$. Let $e$ be a linear equivalence of $F$ and $E$. Then the preimage equivalence of $L$ and $e$ is a linear equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {L}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{comap} (L , \operatorname{toLinearMap} (e))}{x_{6}})}$.

ZSpan.ceildefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $K$ and $E$. Let $m$ be an element of $E$. Then $\operatorname{ceil}$ applied to $b$ and $m$ is an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (\Integer , \operatorname{range} (\operatorname{coe} (b)))}{x_{7}})}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {\operatorname{ceil} (\operatorname{coe} (\operatorname{repr} (b), m , i))}{\operatorname{restrictScalars} (\Integer , b , i)})}$.

ZSpan.floordefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the floor of b and m (from the name)

English

Let $b$ be a basis of $K$ and $E$. Let $m$ be an element of $E$. Then the floor of $b$ and $m$ is an element of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{span} (\Integer , \operatorname{range} (\operatorname{coe} (b)))}{x_{7}})}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{i}{(\HSMulhSMulMACRoAL {\operatorname{floor} (\operatorname{coe} (\operatorname{repr} (b), m , i))}{\operatorname{restrictScalars} (\Integer , b , i)})}$.

ZSpan.fractdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $K$ and $E$. Let $m$ be an element of $E$. Then $\operatorname{fract}$ applied to $b$ and $m$ is an element of $E$ defined as the difference between $m$ and the floor of $b$ and $m$.

ZSpan.fractRestrictdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $K$ and $E$. Let $x_{7}$ be an element of $E$. Then $\operatorname{fractRestrict}$ applied to $b$ and $x_{7}$ is an element of the fundamental domain of $b$ defined as $\operatorname{fract}$ applied to $b$ and $x_{7}$.

ZSpan.fundamentalDomaindefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the fundamental domain of b (from the name)

English

Let $b$ be a basis of $K$ and $E$. Then the fundamental domain of $b$ is an element of $\wp E$ defined as $\operatorname{ofPred}$ applied to the function that maps $m$ to the proposition that for all elements $i$ of $x$, $\operatorname{coe}$ applied to the representation of $b$, $m$ and $i$ is an element of $\operatorname{Ico}$ applied to $0$ and $1$.

ZSpan.quotientEquivdefMathlib.Algebra.Module.ZLattice.Basic, function or constant

Wording

the quotient equivalence of b (from the name)

English

Let $b$ be a basis of $K$ and $E$. Then the quotient equivalence of $b$ is an equivalence from the set of quotients of $E$ and the span of $\Integer$ and the range of $\operatorname{coe}$ applied to $b$ to the set of elements of the fundamental domain of $b$.

Mathlib.Algebra.Module.ZLattice.Covolume

ZLattice.covolumedefMathlib.Algebra.Module.ZLattice.Covolume, function or constant

Wording

no wording

English

Let $L$ be a submodule of $\Integer$ and $E$. Let $x_{2}$ be an element of $\mathrm{autoParam}$ applied to the set of measures of $E$ and $\mathrm{ZLattice\_\_covolume\_\_\_auto\_1}$. Then $\operatorname{covolume}$ applied to $L$ and $x_{2}$ is a real number defined as $\operatorname{toReal}$ applied to $\operatorname{addCovolume}$ applied to $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {L}{x_{3}})}$, $E$ and $x_{2}$.

Mathlib.Algebra.Module.ZLattice.Summable

ZLattice.normBounddefMathlib.Algebra.Module.ZLattice.Summable, function or constant

Wording

the norm bound of b (from the name)

English

Let $b$ be a basis of $\Integer$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {L}{x_{3}})}$. Then the norm bound of $b$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{ZLattice\_\_exists\_forall\_abs\_repr\_le\_norm}$ applied to $b$.

ZLattice.tsumNormRPowBounddefMathlib.Algebra.Module.ZLattice.Summable, function or constant

Wording

the sum norm power bound of L (from the name)

English

Let $L$ be a submodule of $\Integer$ and $E$. Then the sum norm power bound of $L$ is a real number defined as $\operatorname{choose}$ applied to $\mathrm{ZLattice\_\_exists\_finsetSum\_norm\_rpow\_le\_tsum}$ applied to $L$.

Mathlib.Algebra.Module.ZMod

AddMonoidHom.toZModLinearMapdefMathlib.Algebra.Module.ZMod, function or constant

Wording

no wording

English

Let $n$ be a natural number. Let $f$ be an additive monoid homomorphism of $M$ and $x$. Then $\operatorname{toZModLinearMap}$ applied to $n$ and $f$ is a linear map of $M$ and $x$.

AddMonoidHom.toZModLinearMapEquivdefMathlib.Algebra.Module.ZMod, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{toZModLinearMapEquiv}$ applied to $n$ is an additive equivalence of the set of additive monoid homomorphisms of $M$ and $x$ and the set of linear maps of $M$ and $x$.

AddSubgroup.toZModSubmoduledefMathlib.Algebra.Module.ZMod, function or constant

Wording

no wording

English

Let $n$ be a natural number. Then $\operatorname{toZModSubmodule}$ applied to $n$ is an order isomorphism of the set of additive subgroups of $M$ and the set of submodules of $\mathrm{ZMod}$ applied to $n$ and $M$.

Mathlib.Algebra.MonoidAlgebra.Basic

AddMonoidAlgebra.comapDomAlgAutdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the preimage domain algebra automorphism of M and G (from the name)

English

Let $R$, $M$ and $G$ be sets. Then the preimage domain algebra automorphism of $M$ and $G$ is a monoid homomorphism of $G$ and the set of algebra isomorphisms of the set of additive monoid algebras of $R$ and $M$ and the set of additive monoid algebras of $R$ and $M$ defined as the composition of $\operatorname{toMultiplicative}$ applied to the domain congruence automorphism of $R$ and $R$ and the additive automorphism of $G$ and $M$.

AddMonoidAlgebra.commAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the commutative algebra isomorphism of R (from the name)

English

Let $R$ be a set. Then the commutative algebra isomorphism of $R$ is an algebra isomorphism of the set of additive monoid algebras of the set of additive monoid algebras of $A$ and $M$ and $N$ and the set of additive monoid algebras of the set of additive monoid algebras of $A$ and $N$ and $M$ defined as the composition of the inverse of the curry algebra isomorphism of $R$ and the composition of the domain congruence of $\operatorname{prodComm}$ and the curry algebra isomorphism of $R$.

AddMonoidAlgebra.curryAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the curry algebra isomorphism of R (from the name)

English

Let $R$ be a set. Then the curry algebra isomorphism of $R$ is an algebra isomorphism of the set of additive monoid algebras of $A$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of additive monoid algebras of the set of additive monoid algebras of $A$ and $N$ and $M$.

AddMonoidAlgebra.domCongrdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the domain congruence of e (from the name)

English

Let $R$ and $A$ be sets. Let $e$ be an additive equivalence of $M$ and $N$. Then the domain congruence of $e$ is an algebra isomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $N$.

AddMonoidAlgebra.domCongrAutdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the domain congruence automorphism of R and A (from the name)

English

Let $R$ and $A$ be sets. Then the domain congruence automorphism of $R$ and $A$ is an additive monoid homomorphism of the set of additive automorphisms of $M$ and $\mathrm{Additive}$ applied to the set of algebra isomorphisms of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $M$.

AddMonoidAlgebra.liftdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the lift of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the lift of $A$ and $M$ is an equivalence from the set of monoid homomorphisms of the set of multiplicatives of $M$ and $A$ to the set of algebra homomorphisms of the set of additive monoid algebras of $R$ and $M$ and $A$.

AddMonoidAlgebra.liftMagmadefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the lift magma of R (from the name)

English

Let $R$ be a set. Then the lift magma of $R$ is an equivalence from the set of multiplicative homomorphisms of the set of multiplicatives of $M$ and $A$ to the set of non unital algebra homomorphisms of the set of additive monoid algebras of $R$ and $M$ and $A$.

AddMonoidAlgebra.liftNCAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be a monoid homomorphism of the set of multiplicatives of $M$ and $B$ such that for all elements $x_{6}$ of $A$, for all multiplicatives $y$ of $M$, $\mathrm{Commute}$ holds for $f$ applied to $x_{6}$ and $g$ applied to $y$. Then $\operatorname{liftNCAlgHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is an algebra homomorphism of the set of additive monoid algebras of $A$ and $M$ and $B$.

AddMonoidAlgebra.mapAlgAutdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map algebra automorphism of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the map algebra automorphism of $R$ and $M$ is a monoid homomorphism of the set of algebra isomorphisms of $A$ and $A$ and the set of algebra isomorphisms of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $M$.

AddMonoidAlgebra.mapAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map algebra isomorphism of e (from the name)

English

Let $R$ and $M$ be sets. Let $e$ be an algebra isomorphism of $A$ and $B$. Then the map algebra isomorphism of $e$ is an algebra isomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $B$ and $M$.

AddMonoidAlgebra.mapAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map algebra homomorphism of M and f (from the name)

English

Let $M$ be a set. Let $f$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $M$ and $f$ is an algebra homomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $B$ and $M$.

AddMonoidAlgebra.mapDomainAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map domain algebra homomorphism of f (from the name)

English

Let $R$ and $A$ be sets. Let $f$ be an additive monoid homomorphism of $M$ and $N$. Then the map domain algebra homomorphism of $f$ is an algebra homomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $N$.

AddMonoidAlgebra.mapDomainNonUnitalAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map domain non unital algebra homomorphism of f (from the name)

English

Let $R$ and $A$ be sets. Let $f$ be an additive homomorphism of $M$ and $N$. Then the map domain non unital algebra homomorphism of $f$ is a non unital algebra homomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $N$.

AddMonoidAlgebra.singleZeroAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the single zero algebra homomorphism (from the name)

English

The single zero algebra homomorphism is an algebra homomorphism of $A$ and the set of additive monoid algebras of $A$ and $M$.

AddMonoidAlgebra.toMultiplicativeAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the multiplicative algebra isomorphism of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the multiplicative algebra isomorphism of $A$ and $M$ is an algebra isomorphism of the set of additive monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and the set of multiplicatives of $M$.

AddMonoidAlgebra.uniqueAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the trivial monoid algebra of R and M (from the docstring)

English

Let $R$ and $M$ be sets. Then the trivial monoid algebra of $R$ and $M$ is an algebra isomorphism of the set of additive monoid algebras of $A$ and $M$ and $A$.

MonoidAlgebra.GroupSMul.linearMapdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the linear map of g (from the name)

English

Let $R$ and $V$ be sets. Let $g$ be an element of $M$. Then the linear map of $g$ is a linear map of $V$ and $V$.

MonoidAlgebra.commAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the commutative algebra isomorphism of R (from the name)

English

Let $R$ be a set. Then the commutative algebra isomorphism of $R$ is an algebra isomorphism of the set of monoid algebras of the set of monoid algebras of $A$ and $M$ and $N$ and the set of monoid algebras of the set of monoid algebras of $A$ and $N$ and $M$ defined as the composition of the inverse of the curry algebra isomorphism of $R$ and the composition of the domain congruence of $\operatorname{prodComm}$ and the curry algebra isomorphism of $R$.

MonoidAlgebra.curryAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the curry algebra isomorphism of R (from the name)

English

Let $R$ be a set. Then the curry algebra isomorphism of $R$ is an algebra isomorphism of the set of monoid algebras of $A$ and $\mathrm{Prod}$ applied to $M$ and $N$ and the set of monoid algebras of the set of monoid algebras of $A$ and $N$ and $M$.

MonoidAlgebra.domCongrdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the domain congruence of e (from the name)

English

Let $R$ and $A$ be sets. Let $e$ be a multiplicative equivalence of $M$ and $N$. Then the domain congruence of $e$ is an algebra isomorphism of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $N$.

MonoidAlgebra.domCongrAutdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the domain congruence automorphism (from the name)

English

The domain congruence automorphism is a monoid homomorphism of the set of multiplicative automorphisms of $M$ and the set of algebra isomorphisms of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $M$.

MonoidAlgebra.equivariantOfLinearOfCommdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

no wording

English

Let $f$ be a linear map of $V$ and $W$ such that for all elements $g$ of $M$, for all elements $v$ of $V$, $\EqtMACRoH {f (\HSMulhSMulMACRoAL {\operatorname{single} (g , 1)}{v})}{\HSMulhSMulMACRoAL {\operatorname{single} (g , 1)}{f (v)}}$. Then $\operatorname{equivariantOfLinearOfComm}$ applied to $f$ and $h_{2}$ is a linear map of $V$ and $W$.

MonoidAlgebra.liftdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the lift of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the lift of $A$ and $M$ is an equivalence from the set of monoid homomorphisms of $M$ and $A$ to the set of algebra homomorphisms of the set of monoid algebras of $R$ and $M$ and $A$.

MonoidAlgebra.liftMagmadefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the lift magma of R (from the name)

English

Let $R$ be a set. Then the lift magma of $R$ is an equivalence from the set of multiplicative homomorphisms of $M$ and $A$ to the set of non unital algebra homomorphisms of the set of monoid algebras of $R$ and $M$ and $A$.

MonoidAlgebra.liftNCAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

no wording

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be a monoid homomorphism of $M$ and $B$ such that for all elements $x_{6}$ of $A$, for all elements $y$ of $M$, $\mathrm{Commute}$ holds for $f$ applied to $x_{6}$ and $g$ applied to $y$. Then $\operatorname{liftNCAlgHom}$ applied to $f$, $g$ and $\mathrm{h\_comm}$ is an algebra homomorphism of the set of monoid algebras of $A$ and $M$ and $B$.

MonoidAlgebra.mapAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map algebra isomorphism of e (from the name)

English

Let $R$ and $M$ be sets. Let $e$ be an algebra isomorphism of $A$ and $B$. Then the map algebra isomorphism of $e$ is an algebra isomorphism of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $B$ and $M$.

MonoidAlgebra.mapAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map algebra homomorphism of M and f (from the name)

English

Let $M$ be a set. Let $f$ be an algebra homomorphism of $A$ and $B$. Then the map algebra homomorphism of $M$ and $f$ is an algebra homomorphism of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $B$ and $M$.

MonoidAlgebra.mapDomainAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map domain algebra homomorphism of f (from the name)

English

Let $R$ and $A$ be sets. Let $f$ be a monoid homomorphism of $M$ and $N$. Then the map domain algebra homomorphism of $f$ is an algebra homomorphism of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $N$.

MonoidAlgebra.mapDomainNonUnitalAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map domain non unital algebra homomorphism of f (from the name)

English

Let $R$ and $A$ be sets. Let $f$ be a multiplicative homomorphism of $M$ and $N$. Then the map domain non unital algebra homomorphism of $f$ is a non unital algebra homomorphism of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $N$.

MonoidAlgebra.mapRangeAlgAutdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the map range algebra automorphism of R and M (from the name)

English

Let $R$ and $M$ be sets. Then the map range algebra automorphism of $R$ and $M$ is a monoid homomorphism of the set of algebra isomorphisms of $A$ and $A$ and the set of algebra isomorphisms of the set of monoid algebras of $A$ and $M$ and the set of monoid algebras of $A$ and $M$.

MonoidAlgebra.singleOneAlgHomdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the single one algebra homomorphism (from the name)

English

The single one algebra homomorphism is an algebra homomorphism of $A$ and the set of monoid algebras of $A$ and $M$.

MonoidAlgebra.toAdditiveAlgEquivdefMathlib.Algebra.MonoidAlgebra.Basic, function or constant

Wording

the additive algebra isomorphism of A and M (from the name)

English

Let $R$, $A$ and $M$ be sets. Then the additive algebra isomorphism of $A$ and $M$ is an algebra isomorphism of the set of monoid algebras of $A$ and $M$ and the set of additive monoid algebras of $A$ and $\mathrm{Additive}$ applied to $M$.