Definitions: Mathlib.Algebra, part 12 of 17

LieAlgebra.centerdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the center of R and L (from the docstring)

English

Let $R$ and $L$ be sets. Then the center of $R$ and $L$ is a Lie ideal of $R$ and $L$ defined as the maximum trivial submodule of $L$ and $L$.

LieModule.IsTrivialclassMathlib.Algebra.Lie.Abelian, predicate

Wording

no wording

English

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

LieModule.kerdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the kernel of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the kernel of $L$ and $M$ is a Lie ideal of $R$ and $L$ defined as the kernel of the end of $L$ and $M$.

LieModule.maxTrivEquivdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the maximum trivial equivalence of e (from the name)

English

Let $e$ be a Lie module equivalence of $M$ and $N$. Then the maximum trivial equivalence of $e$ is a Lie module equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{maxTrivSubmodule} (L , M)}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{maxTrivSubmodule} (L , N)}{x_{10}})}$.

LieModule.maxTrivHomdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the maximum trivial homomorphism of f (from the name)

English

Let $f$ be a Lie module homomorphism of $M$ and $N$. Then the maximum trivial homomorphism of $f$ is a Lie module homomorphism of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{maxTrivSubmodule} (L , M)}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{maxTrivSubmodule} (L , N)}{x_{10}})}$.

LieModule.maxTrivLinearMapEquivLieModuleHomdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the maximum trivial linear map equivalence Lie module homomorphism (from the name)

English

The maximum trivial linear map equivalence Lie module homomorphism is a linear equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{maxTrivSubmodule} (L , \mathrm{LinearMap} (M , N))}{x_{9}})}$ and the set of Lie module homomorphisms of $M$ and $N$.

LieModule.maxTrivSubmoduledefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the maximum trivial submodule of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the maximum trivial submodule of $L$ and $M$ is a Lie submodule of $L$ and $M$.

TrivialLieModuledefMathlib.Algebra.Lie.Abelian, type

Wording

trivial Lie module of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then a trivial Lie module of $L$ and $M$ is an element of the function that maps $R$, $L$ and $M$ to $M$.

TrivialLieModule.equivdefMathlib.Algebra.Lie.Abelian, function or constant

Wording

the equivalence of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the equivalence of $L$ and $M$ is a linear equivalence of the set of trivial Lie modules of $L$ and $M$ and $M$ defined as the identity map of $R$ and $M$.

Mathlib.Algebra.Lie.AdjointAction.Derivation

LieDerivation.addefMathlib.Algebra.Lie.AdjointAction.Derivation, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\operatorname{ad}$ applied to $R$ and $L$ is a Lie homomorphism of $L$ and the set of Lie derivations of $L$ and $L$.

Mathlib.Algebra.Lie.BaseChange

LieAlgebra.ExtendScalars.mapdefMathlib.Algebra.Lie.BaseChange, function or constant

Wording

the Lie algebra homomorphism induced by an algebra map of f and g (from the docstring)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Let $g$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Then the Lie algebra homomorphism induced by an algebra map of $f$ and $g$ is a Lie homomorphism of the set of tensor products of $A$ and $L$ and the set of tensor products of $B$ and $\mathrm{L'}$.

LieSubmodule.baseChangedefMathlib.Algebra.Lie.BaseChange, function or constant

Wording

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

English

Let $A$ be a set. Let $N$ be a Lie submodule of $L$ and $M$. Then the base change of $A$ and $N$ is a Lie submodule of the set of tensor products of $A$ and $L$ and the set of tensor products of $A$ and $M$.

Mathlib.Algebra.Lie.Basic

IsLieTowerclassMathlib.Algebra.Lie.Basic, predicate

Wording

no wording

English

Let $x$, $x_{1}$ and $M$ be sets. Then we can say that $\mathrm{IsLieTower}$ holds for $x$, $x_{1}$ and $M$.

LieAlgebraclassMathlib.Algebra.Lie.Basic, predicate

Wording

no wording

English

Let $R$ and $L$ be sets. Then we can say that $\mathrm{LieAlgebra}$ holds for $R$ and $L$.

LieEquivstructureMathlib.Algebra.Lie.Basic, type

Wording

Lie equivalence of L and #3 (from the name)

English

Let $R$, $L$ and $\mathrm{L'}$ be sets. Then the Lie equivalences of $L$ and $\mathrm{L'}$ are a basic type.

LieEquiv.invFundefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse function of self and x5 (from the docstring)

English

Let $\mathrm{self}$ be a Lie equivalence of $L$ and $\mathrm{L'}$. Let $x_{5}$ be an element of $\mathrm{L'}$. Then the inverse function of $\mathrm{self}$ and $x_{5}$ is an element of $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{5}$.

LieEquiv.ofBijectivedefMathlib.Algebra.Lie.Basic, function or constant

Wording

the Lie equivalence of f and h (from the name)

English

Let $f$ be a Lie homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is bijective. Then the Lie equivalence of $f$ and $h$ is a Lie equivalence of $x$ and $x_{1}$.

LieEquiv.refldefMathlib.Algebra.Lie.Basic, function or constant

Wording

the identity (from the name)

English

The identity is a Lie equivalence of $x$ and $x$ defined as $1$.

LieEquiv.symmdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse of e (from the name)

English

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

LieEquiv.toLinearEquivdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the linear equivalence of f (from the name)

English

Let $f$ be a Lie equivalence of $x$ and $x_{1}$. Then the linear equivalence of $f$ is a linear equivalence of $x$ and $x_{1}$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLieHom}$ applied to $f$, $\operatorname{invFun}$ applied to $f$, $\mathrm{LieEquiv\_\_left\_inv}$ applied to $f$ and $\mathrm{LieEquiv\_\_right\_inv}$ applied to $f$.

LieEquiv.transdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the composition of x10 and x11 (from the name)

English

Let $x_{10}$ be a Lie equivalence of $x$ and $x_{1}$. Let $x_{11}$ be a Lie equivalence of $x_{1}$ and $x_{2}$. Then the composition of $x_{10}$ and $x_{11}$ is a Lie equivalence of $x$ and $x_{2}$.

LieHomstructureMathlib.Algebra.Lie.Basic, type

Wording

Lie homomorphism of L and #3 (from the name)

English

Let $R$, $L$ and $\mathrm{L'}$ be sets. Then the Lie homomorphisms of $L$ and $\mathrm{L'}$ are a basic type.

LieHom.compdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a Lie homomorphism of $x_{1}$ and $x_{2}$. Let $g$ be a Lie homomorphism of $x$ and $x_{1}$. Then the composition of $f$ and $g$ is a Lie homomorphism of $x$ and $x_{2}$.

LieHom.iddefMathlib.Algebra.Lie.Basic, function or constant

Wording

the identity map (from the docstring)

English

The identity map is a Lie homomorphism of $x$ and $x$.

LieHom.inversedefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a Lie homomorphism of $x$ and $x_{1}$. Let $g$ be a function from elements of $x_{1}$ to elements of $x$ 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 Lie homomorphism of $x_{1}$ and $x$.

LieModuleclassMathlib.Algebra.Lie.Basic, predicate

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then we can say that $\mathrm{LieModule}$ holds for $R$, $L$ and $M$.

LieModuleEquivstructureMathlib.Algebra.Lie.Basic, type

Wording

Lie module equivalence of M and N (from the name)

English

Let $R$, $L$, $M$ and $N$ be sets. Then the Lie module equivalences of $M$ and $N$ are a basic type.

LieModuleEquiv.invFundefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse function of self and x8 (from the docstring)

English

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

LieModuleEquiv.refldefMathlib.Algebra.Lie.Basic, function or constant

Wording

the identity (from the name)

English

The identity is a Lie module equivalence of $M$ and $M$ defined as $1$.

LieModuleEquiv.symmdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse of e (from the name)

English

Let $e$ be a Lie module equivalence of $M$ and $N$. Then the inverse of $e$ is a Lie module equivalence of $N$ and $M$.

LieModuleEquiv.toEquivdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be a Lie module equivalence of $M$ and $N$. Then the equivalence of $e$ is an equivalence from $M$ to $N$ defined as $\operatorname{mk}$ applied to $\operatorname{toFun}$ applied to $\operatorname{toAddHom}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLieModuleHom}$ applied to $e$, $\operatorname{invFun}$ applied to $e$, $\mathrm{LieModuleEquiv\_\_left\_inv}$ applied to $e$ and $\mathrm{LieModuleEquiv\_\_right\_inv}$ applied to $e$.

LieModuleEquiv.toLinearEquivdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the linear equivalence of e (from the name)

English

Let $e$ be a Lie module equivalence of $M$ and $N$. Then the linear equivalence of $e$ is a linear equivalence of $M$ and $N$ defined as $\operatorname{mk}$ applied to $\operatorname{toLinearMap}$ applied to $\operatorname{toLieModuleHom}$ applied to $e$, $\operatorname{invFun}$ applied to $e$, $\mathrm{LieModuleEquiv\_\_left\_inv}$ applied to $e$ and $\mathrm{LieModuleEquiv\_\_right\_inv}$ applied to $e$.

LieModuleEquiv.transdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the composition of x11 and x12 (from the name)

English

Let $x_{11}$ be a Lie module equivalence of $M$ and $N$. Let $x_{12}$ be a Lie module equivalence of $N$ and $P$. Then the composition of $x_{11}$ and $x_{12}$ is a Lie module equivalence of $M$ and $P$.

LieModuleHomstructureMathlib.Algebra.Lie.Basic, type

Wording

Lie module homomorphism of M and N (from the name)

English

Let $R$, $L$, $M$ and $N$ be sets. Then the Lie module homomorphisms of $M$ and $N$ are a basic type.

LieModuleHom.compdefMathlib.Algebra.Lie.Basic, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a Lie module homomorphism of $N$ and $P$. Let $g$ be a Lie module homomorphism of $M$ and $N$. Then the composition of $f$ and $g$ is a Lie module homomorphism of $M$ and $P$.

LieModuleHom.iddefMathlib.Algebra.Lie.Basic, function or constant

Wording

the identity map (from the docstring)

English

The identity map is a Lie module homomorphism of $M$ and $M$.

LieModuleHom.inversedefMathlib.Algebra.Lie.Basic, function or constant

Wording

the inverse of f and g (from the name)

English

Let $f$ be a Lie module homomorphism of $M$ and $N$. Let $g$ be a function from elements of $N$ 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 Lie module homomorphism of $N$ and $M$.

LieRingclassMathlib.Algebra.Lie.Basic, predicate

Wording

L is a Lie ring (from the name)

English

Let $L$ be a set. Then we can say that $L$ is a Lie ring.

LieRingModuleclassMathlib.Algebra.Lie.Basic, predicate

Wording

no wording

English

Let $L$ and $M$ be sets. Then we can say that $\mathrm{LieRingModule}$ holds for $L$ and $M$.

LieRingModule.toEnddefMathlib.Algebra.Lie.Basic, function or constant

Wording

the end of L and M (from the name)

English

Let $L$ and $M$ be sets. Then the end of $L$ and $M$ is an additive monoid homomorphism of $L$ and the set of additive monoid homomorphisms of $M$ and $M$.

Mathlib.Algebra.Lie.Basis.Base

LieAlgebra.Basis.basedefMathlib.Algebra.Lie.Basis.Base, function or constant

Wording

the base of b (from the name)

English

Let $b$ be a basis of $x_{3}$ and $H$. Then the base of $b$ is a base of the root system of $H$ defined as $\operatorname{mk'}$ applied to the root system of $H$, the range of $\operatorname{baseSupp'}$ applied to $b$, $\mathrm{LieAlgebra\_\_Basis\_\_linearIndepOn\_root\_baseSupp}$ applied to $b$ and $\mathrm{LieAlgebra\_\_Basis\_\_root\_mem\_or\_mem\_neg}$ applied to $b$.

LieAlgebra.Basis.baseSupp'defMathlib.Algebra.Lie.Basis.Base, function or constant

Wording

the base support of b and i (from the name)

English

Let $b$ be a basis of $x_{3}$ and $H$. Let $i$ be an element of $x_{3}$. Then the base support of $b$ and $i$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{root}}{x_{5}})}$.

LieAlgebra.Basis.baseSupportEquivdefMathlib.Algebra.Lie.Basis.Base, function or constant

Wording

the support of b (from the docstring)

English

Let $b$ be a basis of $x_{3}$ and $H$. Then the support of $b$ is an element of $\EquivMACRoAE {x_{3}}{(\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{support} (\operatorname{base} (b))}{x_{5}})})}$.

LieAlgebra.equivOfRootSystemEquivdefMathlib.Algebra.Lie.Basis.Base, function or constant

Wording

the equivalence of e (from the name)

English

Let $e$ be an equivalence of the root system of $H$ and the root system of $x_{6}$. Then the equivalence of $e$ is a Lie equivalence of $L$ and $x_{3}$.

Mathlib.Algebra.Lie.Basis.Basic

LieAlgebra.BasisstructureMathlib.Algebra.Lie.Basis.Basic, type

Wording

basis of x and H (from the name)

English

Let $x$ be a set. Let $H$ be a Lie subalgebra of $R$ and $L$. Then the bases of $x$ and $H$ are a basic type.

LieAlgebra.Basis.AdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a basis of $x$ and $H$. Then there is a matrix of $x$ and $\Integer$. Proof. Let $\mathrm{self}$ be arbitrary. By self. By LieAlgebra__Basis__proj0.

LieAlgebra.Basis.baseSuppdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

the base support of b and i (from the name)

English

Let $b$ be a basis of $x$ and $H$. Let $i$ be an element of $x$. Then the base support of $b$ and $i$ is a dual of $R$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ defined as $\FinsetSum {\FinsetunivMACRoAC}{j}{(\HSMulhSMulMACRoAL {\operatorname{A} (b , i , j)}{\operatorname{coord} (\operatorname{map} (\operatorname{span} (\operatorname{linInd} (b)), \operatorname{symm} (\operatorname{ofEq} (\operatorname{toSubmodule} (H), \operatorname{span} (R , \operatorname{range} (\operatorname{h} (b)))))), j)})}$.

LieAlgebra.Basis.borelLowerdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $x$ and $H$. Then $\operatorname{borelLower}$ applied to $b$ is a Lie submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $L$.

LieAlgebra.Basis.borelUpperdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $x$ and $H$. Then $\operatorname{borelUpper}$ applied to $b$ is a Lie submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $L$.

LieAlgebra.Basis.edefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a basis of $x$ and $H$. Let $x_{4}$ be an element of $x$. Then $\operatorname{e}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $L$ defined as $\operatorname{proj2}$ applied to $\mathrm{self}$ and $x_{4}$.

LieAlgebra.Basis.fdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a basis of $x$ and $H$. Let $x_{4}$ be an element of $x$. Then $\operatorname{f}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $L$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$ and $x_{4}$.

LieAlgebra.Basis.hdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a basis of $x$ and $H$. Let $x_{4}$ be an element of $x$. Then $\operatorname{h}$ applied to $\mathrm{self}$ and $x_{4}$ is an element of $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{4}$.

LieAlgebra.Basis.h'defMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

no wording

English

Let $b$ be a basis of $x$ and $H$. Let $i$ be an element of $x$. Then $\operatorname{h'}$ applied to $b$ and $i$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ defined as $\operatorname{h}$ applied to $b$ and $i$.

LieAlgebra.Basis.symmdefMathlib.Algebra.Lie.Basis.Basic, function or constant

Wording

the inverse of b (from the name)

English

Let $b$ be a basis of $x$ and $H$. Then the inverse of $b$ is a basis of $x$ and $H$.

Mathlib.Algebra.Lie.Basis.Prod

LieAlgebra.Basis.equivOfReindexdefMathlib.Algebra.Lie.Basis.Prod, function or constant

Wording

the equivalence of x10 and x13 (from the name)

English

Let $x_{4}$ be an equivalence from $x$ to $x_{1}$. Let $x_{10}$ be a basis of $x$ and $x_{9}$. Let $x_{13}$ be a basis of $x_{1}$ and $x_{12}$ such that $\EqtMACRoH {\operatorname{reindex} (x_{4} , x_{4} , \operatorname{A} (x_{10}))}{\operatorname{A} (x_{13})}$. Then the equivalence of $x_{10}$ and $x_{13}$ is a Lie equivalence of $x_{2}$ and $x_{3}$.

Mathlib.Algebra.Lie.CartanSubalgebra

LieSubalgebra.IsCartanSubalgebraclassMathlib.Algebra.Lie.CartanSubalgebra, predicate

Wording

H is a Cartan subalgebra (from the name)

English

Let $H$ be a Lie subalgebra of $R$ and $L$. Then we can say that $H$ is a Cartan subalgebra.

LieSubmodule.IsUcsLimitdefMathlib.Algebra.Lie.CartanSubalgebra, predicate

Wording

no wording

English

Let $N$ be a Lie submodule of $L$ and $M$. Then $\operatorname{IsUcsLimit}$ holds for $N$, if there exists a natural number $k$, such that for all natural numbers $l$, if $k \leq l$, then $\operatorname{ucs}$ applied to $l$ and the bottom is equal to $N$.

Mathlib.Algebra.Lie.Character

LieAlgebra.LieCharacterdefMathlib.Algebra.Lie.Character, type

Wording

Lie character of R and L (from the name)

English

Let $R$ and $L$ be sets. Then a Lie character of $R$ and $L$ is an element of the function that maps $R$ and $L$ to the set of Lie homomorphisms of $L$ and $R$.

LieAlgebra.lieCharacterEquivLinearDualdefMathlib.Algebra.Lie.Character, function or constant

Wording

the Lie character equivalence linear dual (from the name)

English

The Lie character equivalence linear dual is an equivalence from the set of Lie characters of $R$ and $L$ to the set of duals of $R$ and $L$.

Mathlib.Algebra.Lie.Classical

LieAlgebra.Orthogonal.JBdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By 2. By 1. By HSMul__hSMul. By 0. By 0. By l. By R. By LieAlgebra__Orthogonal__JD. By Matrix__fromBlocks.

LieAlgebra.Orthogonal.JDdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By 0. By 1. By 1. By 0. By Matrix__fromBlocks.

LieAlgebra.Orthogonal.PBdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By 1. By 0. By 0. By l. By R. By LieAlgebra__Orthogonal__PD. By Matrix__fromBlocks.

LieAlgebra.Orthogonal.PDdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By 1. By 1. By Neg__neg. By 1. By 1. By Matrix__fromBlocks.

LieAlgebra.Orthogonal.PsodefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $p$, $q$ and $R$ be sets. Let $i$ be an element of $R$. Then there is a matrix of $\mathrm{Sum}$ applied to $p$ and $q$ and $R$. Proof. Let $p$ be arbitrary. Let $q$ be arbitrary. Let $R$ be arbitrary. Let $i$ be arbitrary. Let $x_{3}$ be arbitrary. By 1. Let $x_{4}$ be arbitrary. By i. By Sum__elim. By Matrix__diagonal.

LieAlgebra.Orthogonal.SdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then there is a matrix of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$. Proof. Let $l$ be arbitrary. Let $R$ be arbitrary. By l. By R. By LieAlgebra__Orthogonal__indefiniteDiagonal.

LieAlgebra.Orthogonal.indefiniteDiagonaldefMathlib.Algebra.Lie.Classical, function or constant

Wording

the indefinite diagonal of q and R (from the name)

English

Let $p$, $q$ and $R$ be sets. Then the indefinite diagonal of $q$ and $R$ is a matrix of $\mathrm{Sum}$ applied to $p$ and $q$ and $R$ defined as the diagonal of $\operatorname{elim}$ applied to the function that maps $x_{3}$ to $1$ and the function that maps $x_{4}$ to $\operatorname{neg}$ applied to $1$.

LieAlgebra.Orthogonal.sodefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $n$ and $R$ be sets. Then $\operatorname{so}$ applied to $n$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $n$ and $R$ defined as the skew adjoint matrice Lie subalgebra of $1$.

LieAlgebra.Orthogonal.so'defMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $p$, $q$ and $R$ be sets. Then $\operatorname{so'}$ applied to $p$, $q$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $p$ and $q$ and $R$ defined as the skew adjoint matrice Lie subalgebra of the indefinite diagonal of $q$ and $R$.

LieAlgebra.Orthogonal.soIndefiniteEquivdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $p$, $q$ and $R$ be sets. Assume that $\EqtMACRoH {i \times i}{\operatorname{neg} (1)}$. Then $\operatorname{soIndefiniteEquiv}$ applied to $p$, $q$, $R$ and $\mathrm{hi}$ is a Lie equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{so'} (p , q , R)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{so} (\mathrm{Sum} (p , q), R)}{x_{6}})}$.

LieAlgebra.Orthogonal.typeBdefMathlib.Algebra.Lie.Classical, function or constant

Wording

the type of l and R (from the name)

English

Let $l$ and $R$ be sets. Then the type of $l$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $\mathrm{Unit}$ and $\mathrm{Sum}$ applied to $l$ and $l$ and $R$ defined as the skew adjoint matrice Lie subalgebra of $\operatorname{JB}$ applied to $l$ and $R$.

LieAlgebra.Orthogonal.typeBEquivSo'defMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then $\operatorname{typeBEquivSo'}$ applied to $l$ and $R$ is a Lie equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{typeB} (l , R)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{so'} (\mathrm{Sum} (\mathrm{Unit} , l), l , R)}{x_{5}})}$.

LieAlgebra.Orthogonal.typeDdefMathlib.Algebra.Lie.Classical, function or constant

Wording

the type of l and R (from the name)

English

Let $l$ and $R$ be sets. Then the type of $l$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$ defined as the skew adjoint matrice Lie subalgebra of $\operatorname{JD}$ applied to $l$ and $R$.

LieAlgebra.Orthogonal.typeDEquivSo'defMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then $\operatorname{typeDEquivSo'}$ applied to $l$ and $R$ is a Lie equivalence of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{typeD} (l , R)}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{so'} (l , l , R)}{x_{5}})}$.

LieAlgebra.SpecialLinear.singledefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $i$ and $j$ be elements of $n$ such that $i \neq j$. Then $\operatorname{single}$ applied to $i$, $j$ and $h$ is a linear map of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{sl} (n , R)}{x_{3}})}$.

LieAlgebra.SpecialLinear.singleSubSingledefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $i$ and $j$ be elements of $n$. Then $\operatorname{singleSubSingle}$ applied to $i$ and $j$ is a linear map of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{sl} (n , R)}{x_{3}})}$.

LieAlgebra.SpecialLinear.sldefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $n$ and $R$ be sets. Then $\operatorname{sl}$ applied to $n$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $n$ and $R$.

LieAlgebra.Symplectic.spdefMathlib.Algebra.Lie.Classical, function or constant

Wording

no wording

English

Let $l$ and $R$ be sets. Then $\operatorname{sp}$ applied to $l$ and $R$ is a Lie subalgebra of $R$ and the set of matrixes of $\mathrm{Sum}$ applied to $l$ and $l$ and $R$ defined as the skew adjoint matrice Lie subalgebra of $\operatorname{J}$ applied to $l$ and $R$.

Mathlib.Algebra.Lie.Cochain

LieModule.Cohomology.d₁₂defMathlib.Algebra.Lie.Cochain, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\mathrm{LieModule\_\_Cohomology\_\_d\_u2081\_\_u2082\_}$ applied to $R$, $L$ and $M$ is a linear map of the set of one cochains of $L$ and $M$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCochain} (R , L , M)}{x_{6}})}$.

LieModule.Cohomology.d₂₃defMathlib.Algebra.Lie.Cochain, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\mathrm{LieModule\_\_Cohomology\_\_d\_u2082\_\_u2083\_}$ applied to $R$, $L$ and $M$ is a linear map of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCochain} (R , L , M)}{x_{6}})}$ and the set of linear maps of $L$ and the set of linear maps of $L$ and the set of linear maps of $L$ and $M$.

LieModule.Cohomology.oneCochaindefMathlib.Algebra.Lie.Cochain, type

Wording

one cochain of L and M (from the name)

English

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

LieModule.Cohomology.twoCochaindefMathlib.Algebra.Lie.Cochain, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\operatorname{twoCochain}$ applied to $R$, $L$ and $M$ is a submodule of $R$ and the set of linear maps of $L$ and the set of linear maps of $L$ and $M$.

LieModule.Cohomology.twoCocycledefMathlib.Algebra.Lie.Cochain, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\operatorname{twoCocycle}$ applied to $R$, $L$ and $M$ is a submodule of $R$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCochain} (R , L , M)}{x_{6}})}$ defined as the kernel of $\mathrm{LieModule\_\_Cohomology\_\_d\_u2082\_\_u2083\_}$ applied to $R$, $L$ and $M$.

Mathlib.Algebra.Lie.Derivation.BaseChange

Lie.Derivation.ofDerivationdefMathlib.Algebra.Lie.Derivation.BaseChange, function or constant

Wording

the derivation of L (from the name)

English

Let $L$ be a set. Then the derivation of $L$ is a Lie homomorphism of the set of derivations of $A$ and $A$ and the set of Lie derivations of the set of tensor products of $A$ and $L$ and the set of tensor products of $A$ and $L$.

Lie.Derivation.ofLieDerivationdefMathlib.Algebra.Lie.Derivation.BaseChange, function or constant

Wording

the derivation of A (from the name)

English

Let $A$ be a set. Then the derivation of $A$ is a Lie homomorphism of the set of Lie derivations of $L$ and $L$ and the set of Lie derivations of the set of tensor products of $A$ and $L$ and the set of tensor products of $A$ and $L$.

Mathlib.Algebra.Lie.Derivation.Basic

LieDerivationstructureMathlib.Algebra.Lie.Derivation.Basic, type

Wording

Lie derivation of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the Lie derivations of $L$ and $M$ are a basic type.

LieDerivation.SMulBracketCommClassclassMathlib.Algebra.Lie.Derivation.Basic, predicate

Wording

no wording

English

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

LieDerivation.coeFnAddMonoidHomdefMathlib.Algebra.Lie.Derivation.Basic, function or constant

Wording

the coercion function additive monoid homomorphism (from the name)

English

The coercion function additive monoid homomorphism is an additive monoid homomorphism of the set of Lie derivations of $L$ and $M$ and the set of functions from elements of $L$ to elements of $M$ defined as $\operatorname{mk}$ applied to $\operatorname{mk}$ applied to $\operatorname{coe}$ and $\mathrm{LieDerivation\_\_coe\_zero}$ and $\mathrm{LieDerivation\_\_coe\_add}$.

LieDerivation.expdefMathlib.Algebra.Lie.Derivation.Basic, function or constant

Wording

the exponential of D and h (from the name)

English

Let $D$ be a Lie derivation of $L$ and $L$ such that $\operatorname{toLinearMap}$ applied to $D$ is nilpotent. Then the exponential of $D$ and $h$ is a Lie equivalence of $L$ and $L$.

LieDerivation.innerdefMathlib.Algebra.Lie.Derivation.Basic, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\operatorname{inner}$ applied to $R$, $L$ and $M$ is a linear map of $M$ and the set of Lie derivations of $L$ and $M$.

LieDerivation.toLinearMapLieHomdefMathlib.Algebra.Lie.Derivation.Basic, function or constant

Wording

the linear map Lie homomorphism of R and L (from the name)

English

Let $R$ and $L$ be sets. Then the linear map Lie homomorphism of $R$ and $L$ is a Lie homomorphism of the set of Lie derivations of $L$ and $L$ and the set of linear maps of $L$ and $L$.

Mathlib.Algebra.Lie.Derivation.Killing

LieDerivation.IsKilling.rangeAdOrthogonaldefMathlib.Algebra.Lie.Derivation.Killing, function or constant

Wording

the orthogonal complement of the inner derivations of R and L (from the docstring)

English

Let $R$ and $L$ be sets. Then the orthogonal complement of the inner derivations of $R$ and $L$ is a Lie submodule of $L$ and the set of Lie derivations of $L$ and $L$.

Mathlib.Algebra.Lie.DirectSum

DirectSum.lieAlgebraComponentdefMathlib.Algebra.Lie.DirectSum, function or constant

Wording

the Lie algebra component of L and j (from the name)

English

Let $R$ and $x$ be sets. Let $L$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the Lie algebra component of $L$ and $j$ is a Lie homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $L$ applied to $i$ and $L$ applied to $j$.

DirectSum.lieAlgebraOfdefMathlib.Algebra.Lie.DirectSum, function or constant

Wording

the Lie algebra of L and j (from the name)

English

Let $R$ and $x$ be sets. Let $L$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the Lie algebra of $L$ and $j$ is a Lie homomorphism of $L$ applied to $j$ and the set of direct sums of $x$ and the function that maps $i$ to $L$ applied to $i$.

DirectSum.lieModuleComponentdefMathlib.Algebra.Lie.DirectSum, function or constant

Wording

the Lie module component of M and j (from the name)

English

Let $R$, $x$ and $L$ be sets. Let $M$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the Lie module component of $M$ and $j$ is a Lie module homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $M$ applied to $i$ and $M$ applied to $j$.

DirectSum.lieModuleOfdefMathlib.Algebra.Lie.DirectSum, function or constant

Wording

the Lie module of M and j (from the name)

English

Let $R$, $x$ and $L$ be sets. Let $M$ be a function from elements of $x$ to sets. Let $j$ be an element of $x$. Then the Lie module of $M$ and $j$ is a Lie module homomorphism of $M$ applied to $j$ and the set of direct sums of $x$ and the function that maps $i$ to $M$ applied to $i$.

DirectSum.toLieAlgebradefMathlib.Algebra.Lie.DirectSum, function or constant

Wording

the Lie algebra of i2 (from the name)

English

Let $\mathrm{L'}$ be a set. Let $f$ be a function from elements $i_{2}$ of $x$ to Lie homomorphisms of $L$ applied to $i_{2}$ and $\mathrm{L'}$ such that the function that maps $i_{1}$ and $j$ to the proposition that for all elements $x_{7}$ of $L$ applied to $i_{1}$, for all elements $y$ of $L$ applied to $j$, the bracket of $f$ applied to $i_{1}$ and $x_{7}$ and $f$ applied to $j$ and $y$ is equal to $0$ is pairwise. Then the Lie algebra of $i_{2}$ is a Lie homomorphism of the set of direct sums of $x$ and the function that maps $i$ to $L$ applied to $i$ and $\mathrm{L'}$.

Mathlib.Algebra.Lie.Engel

LieAlgebra.IsEngeliandefMathlib.Algebra.Lie.Engel, predicate

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\operatorname{IsEngelian}$ holds for $R$ and $L$, if for all sets $M$, for all elements $x_{3}$ of $\mathrm{AddCommGroup}$ applied to $M$, for all elements $x_{4}$ of $\mathrm{Module}$ applied to $R$ and $M$, for all elements $x_{5}$ of $\mathrm{LieRingModule}$ applied to $L$ and $M$, for all elements $h$ of $\mathrm{Proof}$ applied to $\mathrm{LieModule}$ applied to $R$, $L$ and $M$, if for all elements $x_{6}$ of $L$, $\operatorname{toEnd}$ applied to $R$, $L$, $M$ and $x_{6}$ is nilpotent, then $L$ is nilpotent.

Mathlib.Algebra.Lie.EngelSubalgebra

LieSubalgebra.engeldefMathlib.Algebra.Lie.EngelSubalgebra, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{3}$ be an element of $L$. Then $\operatorname{engel}$ applied to $R$ and $x_{3}$ is a Lie subalgebra of $R$ and $L$.

Mathlib.Algebra.Lie.Extension

LieAlgebra.ExtensionstructureMathlib.Algebra.Lie.Extension, type

Wording

type of all Lie extensions of M by N (from the docstring)

English

Let $R$, $N$ and $M$ be sets. Then the types of all Lie extensions of $M$ by $N$ are a basic type.

LieAlgebra.Extension.LdefMathlib.Algebra.Lie.Extension, type

Wording

no wording

English

Let $\mathrm{self}$ be a type of all Lie extensions of $M$ by $N$. Then an element of $\operatorname{L}$ applied to $\mathrm{self}$ is an element of the function that maps $\mathrm{self}$ to $\operatorname{proj0}$ applied to $\mathrm{self}$.

LieAlgebra.Extension.incldefMathlib.Algebra.Lie.Extension, function or constant

Wording

the inclusion homomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be a type of all Lie extensions of $M$ by $N$. Then the inclusion homomorphism of $\mathrm{self}$ is a Lie homomorphism of $N$ and $\operatorname{L}$ applied to $\mathrm{self}$ defined as $\operatorname{proj3}$ applied to $\mathrm{self}$.

LieAlgebra.Extension.ofAlgdefMathlib.Algebra.Lie.Extension, function or constant

Wording

the extension of c (from the name)

English

Let $c$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{6}})}$. Then the extension of $c$ is a Lie equivalence of $\operatorname{ofTwoCocycle}$ applied to $c$ and $\operatorname{L}$ applied to the extension of $c$ defined as the identity.

LieAlgebra.Extension.ofTwoCocycledefMathlib.Algebra.Lie.Extension, function or constant

Wording

the extension of c (from the name)

English

Let $c$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{6}})}$. Then the extension of $c$ is a type of all Lie extensions of $L$ by $M$.

LieAlgebra.Extension.oneCochainOfTwoSplittingdefMathlib.Algebra.Lie.Extension, function or constant

Wording

the one cochain of E (from the name)

English

Let $E$ be a type of all Lie extensions of $L$ by $M$ such that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to the projection homomorphism of $E$ and $\operatorname{coe}$ applied to $x_{5}$ and $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to the projection homomorphism of $E$ and $\operatorname{coe}$ applied to $x_{6}$. Then the one cochain of $E$ is an one cochain of $L$ and $M$.

LieAlgebra.Extension.projdefMathlib.Algebra.Lie.Extension, function or constant

Wording

the projection homomorphism of self (from the docstring)

English

Let $\mathrm{self}$ be a type of all Lie extensions of $M$ by $N$. Then the projection homomorphism of $\mathrm{self}$ is a Lie homomorphism of $\operatorname{L}$ applied to $\mathrm{self}$ and $M$ defined as $\operatorname{proj4}$ applied to $\mathrm{self}$.

LieAlgebra.Extension.toKerdefMathlib.Algebra.Lie.Extension, function or constant

Wording

the Lie algebra isomorphism from the kernel of E (from the docstring)

English

Let $E$ be a type of all Lie extensions of $L$ by $M$. Then the Lie algebra isomorphism from the kernel of $E$ is a Lie equivalence of $M$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{ker} (\operatorname{proj} (E))}{x_{5}})}$.

LieAlgebra.Extension.twoCocycleOfdefMathlib.Algebra.Lie.Extension, function or constant

Wording

no wording

English

Let $E$ be a type of all Lie extensions of $L$ by $M$ such that $\operatorname{LeftInverse}$ holds for $\operatorname{coe}$ applied to the projection homomorphism of $E$ and $\operatorname{coe}$ applied to $s$. Then $\operatorname{twoCocycleOf}$ applied to $E$ and $\mathrm{hs}$ is an element of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{5}})}$.

LieAlgebra.IsExtensionclassMathlib.Algebra.Lie.Extension, predicate

Wording

i is an extension (from the docstring)

English

Let $i$ be a Lie homomorphism of $N$ and $L$. Let $p$ be a Lie homomorphism of $L$ and $M$. Then we can say that $i$ is an extension.

LieAlgebra.IsExtension.extensiondefMathlib.Algebra.Lie.Extension, function or constant

Wording

the extension of h (from the name)

English

Assume that $i$ is an extension. Then the extension of $h$ is a type of all Lie extensions of $M$ by $N$ defined as $\operatorname{mk}$ applied to $L$, $x_{1}$, $x_{2}$, $i$, $p$ and $h$.

LieAlgebra.IsExtension.kerEquivRangedefMathlib.Algebra.Lie.Extension, function or constant

Wording

the equivalence from the kernel of the projection of i and p (from the docstring)

English

Let $i$ be a Lie homomorphism of $N$ and $L$. Let $p$ be a Lie homomorphism of $L$ and $M$. Then the equivalence from the kernel of the projection of $i$ and $p$ is a linear equivalence of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{ker} (p)}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{range} (i)}{x_{8}})}$.

LieAlgebra.LieEquiv.ofCoboundarydefMathlib.Algebra.Lie.Extension, function or constant

Wording

the Lie equivalence of x6 and h1 (from the name)

English

Let $c$ be an element of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{10}})}$. Let $\mathrm{c'}$ be an element of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{9}})}$. Let $x_{6}$ be an one cochain of $L$ and $M$ such that $\EqtMACRoH {\mathrm{c'}}{c + \mathrm{LieModule\_\_Cohomology\_\_d\_u2081\_\_u2082\_\_\_app} (R , L , M , x_{6})}$. Then the Lie equivalence of $\mathrm{c'}$ and $x_{6}$ is a Lie equivalence of $\operatorname{ofTwoCocycle}$ applied to $c$ and $\operatorname{ofTwoCocycle}$ applied to $\mathrm{c'}$.

LieAlgebra.ofProddefMathlib.Algebra.Lie.Extension, function or constant

Wording

the Lie algebra of c (from the name)

English

Let $c$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{6}})}$. Then the Lie algebra of $c$ is an element of $\EquivMACRoAE {\mathrm{Prod} (L , M)}{\operatorname{ofTwoCocycle} (c)}$.

LieAlgebra.ofTwoCocyclestructureMathlib.Algebra.Lie.Extension, type

Wording

no wording

English

Let $c$ be an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , L , M)}{x_{6}})}$. Then the elements of $\operatorname{ofTwoCocycle}$ applied to $c$ are a basic type.

LieAlgebra.ofTwoCocycle.carrierdefMathlib.Algebra.Lie.Extension, function or constant

Wording

the carrier of self (from the name)

English

Let $\mathrm{self}$ be an element of $\operatorname{ofTwoCocycle}$ applied to $c$. Then the carrier of $\mathrm{self}$ is an element of $\mathrm{Prod}$ applied to $L$ and $M$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

Mathlib.Algebra.Lie.Free

FreeLieAlgebradefMathlib.Algebra.Lie.Free, type

Wording

free Lie algebra of R and X (from the name)

English

Let $R$ and $X$ be sets. Then a free Lie algebra of $R$ and $X$ is an element of the function that maps $R$ and $X$ to $\mathrm{Quot}$ applied to $\operatorname{Rel}$ applied to $R$ and $X$.

FreeLieAlgebra.RelinductiveMathlib.Algebra.Lie.Free, predicate

Wording

no wording

English

Let $R$ and $X$ be sets. Let $x_{1}$ and $x_{2}$ be elements of $\mathrm{FreeNonUnitalNonAssocAlgebra}$ applied to $R$ and $X$. Then we can say that $\operatorname{Rel}$ holds for $R$, $X$, $x_{1}$ and $x_{2}$.

FreeLieAlgebra.Rel.belowinductiveMathlib.Algebra.Lie.Free, predicate

Wording

no wording

English

Assume that $\operatorname{Rel}$ holds for $R$, $X$, $x_{1}$ and $x_{2}$. Then we can say that $\operatorname{below}$ holds for $t$.

FreeLieAlgebra.liftdefMathlib.Algebra.Lie.Free, function or constant

Wording

the lift of R (from the name)

English

Let $R$ be a set. Then the lift of $R$ is an equivalence from the set of functions from elements of $X$ to elements of $L$ to the set of Lie homomorphisms of the set of free Lie algebras of $R$ and $X$ and $L$.

FreeLieAlgebra.mkdefMathlib.Algebra.Lie.Free, function or constant

Wording

no wording

English

Let $R$ be a set. Then $\operatorname{mk}$ applied to $R$ is a non unital algebra homomorphism of $\mathrm{FreeNonUnitalNonAssocAlgebra}$ applied to $R$ and $X$ and the set of commutator rings of the set of free Lie algebras of $R$ and $X$.

FreeLieAlgebra.ofdefMathlib.Algebra.Lie.Free, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an element of $X$. Then $\operatorname{of}$ applied to $R$ and $x_{1}$ is a free Lie algebra of $R$ and $X$ defined as $\operatorname{mk}$ applied to $\operatorname{Rel}$ applied to $R$ and $X$ and $\operatorname{of}$ applied to $R$ and $x_{1}$.

FreeLieAlgebra.universalEnvelopingEquivFreeAlgebradefMathlib.Algebra.Lie.Free, function or constant

Wording

the universal enveloping algebra of the free Lie algebra of R and X (from the docstring)

English

Let $R$ and $X$ be sets. Then the universal enveloping algebra of the free Lie algebra of $R$ and $X$ is an algebra isomorphism of the set of universal enveloping algebras of $R$ and the set of free Lie algebras of $R$ and $X$ and the set of free algebras of $R$ and $X$.

Mathlib.Algebra.Lie.Graded

DirectSum.decomposeLieEquivdefMathlib.Algebra.Lie.Graded, function or constant

Wording

no wording

English

Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $L$. Then $\operatorname{decomposeLieEquiv}$ applied to $x_{6}$ is a Lie equivalence of $L$ and the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{8}})}$.

GradedLieAlgebraclassMathlib.Algebra.Lie.Graded, predicate

Wording

x6 is a graded Lie algebra (from the name)

English

Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $L$. Then we can say that $x_{6}$ is a graded Lie algebra.

GradedLieModuleclassMathlib.Algebra.Lie.Graded, predicate

Wording

no wording

English

Let $x_{7}$ be a function from elements of $x$ to submodules of $R$ and $L$. Let $x_{13}$ be a function from elements of $x_{1}$ to submodules of $R$ and $M$. Then we can say that $\mathrm{GradedLieModule}$ holds for $x_{7}$ and $x_{13}$.

LieDerivation.ofGradingdefMathlib.Algebra.Lie.Graded, function or constant

Wording

the Lie derivation of x6 and x8 (from the name)

English

LieDerivation.ofGradingSumdefMathlib.Algebra.Lie.Graded, function or constant

Wording

the Lie derivation of x6 and x8 (from the name)

English

Let $x_{6}$ be a function from elements of $x$ to submodules of $R$ and $L$. Let $x_{8}$ be an additive monoid homomorphism of $x$ and $R$. Then the Lie derivation of $x_{6}$ and $x_{8}$ is a Lie derivation of the set of direct sums of $x$ and the function that maps $i$ to $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{6} (i)}{x_{9}})}$ and the set of direct sums of $x$ and the function that maps $i_{1}$ to $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{6} (i_{1})}{x_{10}})}$.

SetLike.GradedBracketclassMathlib.Algebra.Lie.Graded, predicate

Wording

no wording

English

Let $x_{8}$ be a function from elements of $x$ to elements of $x_{2}$. Let $x_{9}$ be a function from elements of $x_{1}$ to elements of $x_{3}$. Then we can say that $\operatorname{GradedBracket}$ holds for $x_{8}$ and $x_{9}$.

Mathlib.Algebra.Lie.Ideal

LieHom.IsIdealMorphismdefMathlib.Algebra.Lie.Ideal, predicate

Wording

f is a ideal morphism (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Then $f$ is an ideal morphism, if the Lie subalgebra of the range of $f$ is equal to the range of $f$.

LieHom.idealRangedefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Then the range of $f$ is a Lie ideal of $R$ and $\mathrm{L'}$ defined as the Lie span of the range of $f$.

LieHom.kerdefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Then the kernel of $f$ is a Lie ideal of $R$ and $L$ defined as the preimage of $f$ and the bottom.

LieIdealdefMathlib.Algebra.Lie.Ideal, type

Wording

Lie ideal of R and L (from the name)

English

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

LieIdeal.comapdefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the preimage of f and J (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Let $J$ be a Lie ideal of $R$ and $\mathrm{L'}$. Then the preimage of $f$ and $J$ is a Lie ideal of $R$ and $L$.

LieIdeal.incldefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the inclusion of I (from the name)

English

Let $I$ be a Lie ideal of $R$ and $L$. Then the inclusion of $I$ is a Lie homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {I}{x_{3}})}$ and $L$ defined as the inclusion of the Lie subalgebra of $I$.

LieIdeal.inclusiondefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $x_{3} \leq x_{4}$. Then the inclusion of $h$ is a Lie homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {x_{3}}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {x_{4}}{x_{6}})}$.

LieIdeal.mapdefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the map of f and I (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Let $I$ be a Lie ideal of $R$ and $L$. Then the map of $f$ and $I$ is a Lie ideal of $R$ and $\mathrm{L'}$ defined as the Lie span of the map of $\operatorname{toLinearMap}$ applied to $f$ and $\operatorname{toSubmodule}$ applied to the Lie subalgebra of $I$.

LieIdeal.toLieSubalgebradefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the Lie subalgebra of I (from the name)

English

Let $R$ and $L$ be sets. Let $I$ be a Lie ideal of $R$ and $L$. Then the Lie subalgebra of $I$ is a Lie subalgebra of $R$ and $L$.

LieIdeal.topEquivdefMathlib.Algebra.Lie.Ideal, function or constant

Wording

the top equivalence (from the name)

English

The top equivalence is a Lie equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $L$ defined as the top equivalence.

Mathlib.Algebra.Lie.InvariantForm

LieAlgebra.InvariantForm.orthogonaldefMathlib.Algebra.Lie.InvariantForm, function or constant

Wording

no wording

English

Let $x_{5}$ be a bilinear form of $R$ and $M$ such that $x_{5}$ is a Lie invariant. Let $N$ be a Lie submodule of $L$ and $M$. Then $\operatorname{orthogonal}$ applied to $x_{5}$, $h$ and $N$ is a Lie submodule of $L$ and $M$.

LinearMap.BilinForm.lieInvariantdefMathlib.Algebra.Lie.InvariantForm, predicate

Wording

x5 is a Lie invariant (from the name)

English

Let $L$ be a set. Let $x_{5}$ be a bilinear form of $R$ and $M$. Then $x_{5}$ is a Lie invariant, if for all elements $x_{6}$ of $L$, for all elements $y$ and $z$ of $M$, $\operatorname{coe}$ applied to $x_{5}$, the bracket of $x_{6}$ and $y$ and $z$ is equal to $\operatorname{neg}$ applied to $\operatorname{coe}$ applied to $x_{5}$, $y$ and the bracket of $x_{6}$ and $z$.

Mathlib.Algebra.Lie.Killing

LieAlgebra.IsKillingclassMathlib.Algebra.Lie.Killing, predicate

Wording

no wording

English

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

Mathlib.Algebra.Lie.LieTheorem

LieModule.weightSpaceOfIsLieTowerdefMathlib.Algebra.Lie.LieTheorem, function or constant

Wording

no wording

English

Let $R$ and $V$ be sets. Let $x_{11}$ be a function from elements of $A$ to elements of $R$. Then $\operatorname{weightSpaceOfIsLieTower}$ applied to $R$, $V$ and $x_{11}$ is a Lie submodule of $L$ and $V$.

Mathlib.Algebra.Lie.Loop

LieAlgebra.LoopAlgebra.residuePairingdefMathlib.Algebra.Lie.Loop, function or constant

Wording

the residue pairing of x5 (from the name)

English

Let $R$, $A$ and $L$ be sets. Let $x_{5}$ be a bilinear form of $R$ and $L$. Then the residue pairing of $x_{5}$ is a bilinear form of $R$ and the set of loop algebras of $A$ and $L$.

LieAlgebra.LoopAlgebra.toFinsuppdefMathlib.Algebra.Lie.Loop, function or constant

Wording

the finitely supported function of A and L (from the name)

English

Let $R$, $A$ and $L$ be sets. Then the finitely supported function of $A$ and $L$ is a linear equivalence of the set of loop algebras of $A$ and $L$ and $\FinsuppMACRoQ {A}{L}$ defined as the equivalence finitely supported function of the standard basis of $A$ and $R$.

LieAlgebra.LoopAlgebra.twoCochainOfBilineardefMathlib.Algebra.Lie.Loop, function or constant

Wording

no wording

English

Let $R$, $A$ and $L$ be sets. Let $x_{5}$ be an inverse bilinear form of $R$ and $L$. Then $\operatorname{twoCochainOfBilinear}$ applied to $R$, $A$, $L$, $x_{5}$ and $h_{1}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCochain} (R , \operatorname{loopAlgebra} (A , L), \mathrm{TrivialLieModule} (\operatorname{loopAlgebra} (A , L), R))}{x_{6}})}$ defined as $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to the residue pairing of $x_{5}$ and $\operatorname{toLinearMap}$ applied to the inverse of the equivalence of the set of loop algebras of $A$ and $L$ and $R$.

LieAlgebra.LoopAlgebra.twoCocycleOfBilineardefMathlib.Algebra.Lie.Loop, function or constant

Wording

no wording

English

Let $R$, $A$ and $L$ be sets. Let $x_{5}$ be a bilinear form of $R$ and $L$ such that $x_{5}$ is a Lie invariant and $x_{5}$ is inverse. Then $\operatorname{twoCocycleOfBilinear}$ applied to $R$, $A$, $L$, $x_{5}$, $h_{1}$ and $h_{2}$ is an element of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{twoCocycle} (R , \operatorname{loopAlgebra} (A , L), \mathrm{TrivialLieModule} (\operatorname{loopAlgebra} (A , L), R))}{x_{6}})}$ defined as $\operatorname{twoCochainOfBilinear}$ applied to $R$, $A$, $L$, $x_{5}$ and $h_{2}$.

LieAlgebra.loopAlgebradefMathlib.Algebra.Lie.Loop, type

Wording

loop algebra of A and L (from the name)

English

Let $R$, $A$ and $L$ be sets. Then a loop algebra of $A$ and $L$ is an element of the function that maps $R$, $A$ and $L$ to the set of tensor products of the set of additive monoid algebras of $R$ and $A$ and $L$.

LieAlgebra.loopAlgebraEquivLaurentdefMathlib.Algebra.Lie.Loop, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\operatorname{loopAlgebraEquivLaurent}$ applied to $R$ and $L$ is a Lie equivalence of the set of loop algebras of $\Integer$ and $L$ and the set of tensor products of the set of Laurent polynomials of $R$ and $L$ defined as the identity.

Mathlib.Algebra.Lie.Matrix

Matrix.lieConjdefMathlib.Algebra.Lie.Matrix, function or constant

Wording

the Lie conjugate of P and h (from the name)

English

Let $P$ be an invertible matrix of $n$ and $R$. Then the Lie conjugate of $P$ and $h$ is a Lie equivalence of the set of matrixes of $n$ and $R$ and the set of matrixes of $n$ and $R$ defined as the composition of the composition of the inverse of the Lie equivalence matrix and the Lie conjugate of the linear equivalence of $P$ and $h$ and the Lie equivalence matrix.

Matrix.reindexLieEquivdefMathlib.Algebra.Lie.Matrix, function or constant

Wording

the reindexing Lie equivalence of e (from the name)

English

Let $e$ be an equivalence from $n$ to $m$. Then the reindexing Lie equivalence of $e$ is a Lie equivalence of the set of matrixes of $n$ and $R$ and the set of matrixes of $m$ and $R$.

lieEquivMatrix'defMathlib.Algebra.Lie.Matrix, function or constant

Wording

the Lie equivalence matrix (from the name)

English

The Lie equivalence matrix is a Lie equivalence of the set of ends of $R$ and the set of functions from elements of $n$ to elements of $R$ and the set of matrixes of $n$ and $R$.

Mathlib.Algebra.Lie.Nilpotent

LieAlgebra.maxNilpotentIdealdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

the maximum nilpotent ideal of R and L (from the name)

English

Let $R$ and $L$ be sets. Then the maximum nilpotent ideal of $R$ and $L$ is a Lie submodule of $L$ and $L$ defined as the maximum nilpotent submodule of $L$ and $L$.

LieIdeal.lcsdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

no wording

English

Let $I$ be a Lie ideal of $R$ and $L$. Let $M$ be a set. Let $k$ be a natural number. Then $\operatorname{lcs}$ applied to $I$, $M$ and $k$ is a Lie submodule of $L$ and $M$ defined as $\operatorname{iterate}$ applied to the function that maps $N$ to the bracket of $I$ and $N$, $k$ and the top.

LieModule.IsNilpotentclassMathlib.Algebra.Lie.Nilpotent, predicate

Wording

L is nilpotent (from the docstring)

English

Let $L$ and $M$ be sets. Then we can say that $L$ is nilpotent.

LieModule.lowerCentralSeriesdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

the lower central series of k (from the name)

English

Let $R$, $L$ and $M$ be sets. Let $k$ be a natural number. Then the lower central series of $k$ is a Lie submodule of $L$ and $M$ defined as $\operatorname{lcs}$ applied to $k$ and the top.

LieModule.lowerCentralSeriesLastdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\operatorname{lowerCentralSeriesLast}$ applied to $R$, $L$ and $M$ is a Lie submodule of $L$ and $M$.

LieModule.maxNilpotentSubmoduledefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

the maximum nilpotent submodule of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the maximum nilpotent submodule of $L$ and $M$ is a Lie submodule of $L$ and $M$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $N$ to the proposition that $L$ is nilpotent.

LieModule.nilpotencyLengthdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

the nilpotency length of L and M (from the name)

English

Let $L$ and $M$ be sets. Then the nilpotency length of $L$ and $M$ is a natural number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $k$ to the proposition that the lower central series of $k$ is equal to the bottom.

LieRing.IsNilpotentdefMathlib.Algebra.Lie.Nilpotent, predicate

Wording

L is nilpotent (from the name)

English

Let $L$ be a set. Then $L$ is nilpotent, if $L$ is nilpotent.

LieSubmodule.lcsdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x_{6}$ be a Lie submodule of $L$ and $M$. Then $\operatorname{lcs}$ applied to $k$ and $x_{6}$ is a Lie submodule of $L$ and $M$ defined as $\operatorname{iterate}$ applied to the function that maps $N$ to the bracket of the top and $N$, $k$ and $x_{6}$.

LieSubmodule.ucsdefMathlib.Algebra.Lie.Nilpotent, function or constant

Wording

no wording

English

Let $k$ be a natural number. Let $x_{6}$ be a Lie submodule of $L$ and $M$. Then $\operatorname{ucs}$ applied to $k$ and $x_{6}$ is a Lie submodule of $L$ and $M$ defined as $\operatorname{iterate}$ applied to $\operatorname{normalizer}$, $k$ and $x_{6}$.

Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra

CommutatorRingdefMathlib.Algebra.Lie.NonUnitalNonAssocAlgebra, type

Wording

commutator ring of L (from the name)

English

Let $L$ be a set. Then a commutator ring of $L$ is an element of the function that maps $L$ to $L$.

LieHom.toNonUnitalAlgHomdefMathlib.Algebra.Lie.NonUnitalNonAssocAlgebra, function or constant

Wording

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

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Then the non unital algebra homomorphism of $f$ is a non unital algebra homomorphism of the set of commutator rings of $L$ and the set of commutator rings of $x_{3}$.

Mathlib.Algebra.Lie.Normalizer

LieSubalgebra.normalizerdefMathlib.Algebra.Lie.Normalizer, function or constant

Wording

the normalizer of H (from the name)

English

Let $H$ be a Lie subalgebra of $R$ and $L$. Then the normalizer of $H$ is a Lie subalgebra of $R$ and $L$.

LieSubmodule.idealizerdefMathlib.Algebra.Lie.Normalizer, function or constant

Wording

no wording

English

Let $N$ be a Lie submodule of $L$ and $M$. Then $\operatorname{idealizer}$ applied to $N$ is a Lie ideal of $R$ and $L$.

LieSubmodule.normalizerdefMathlib.Algebra.Lie.Normalizer, function or constant

Wording

the normalizer of N (from the docstring)

English

Let $N$ be a Lie submodule of $L$ and $M$. Then the normalizer of $N$ is a Lie submodule of $L$ and $M$.

Mathlib.Algebra.Lie.OfAssociative

AlgEquiv.toLieEquivdefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

the Lie equivalence of e (from the name)

English

Let $e$ be an algebra isomorphism of $x$ and $x_{1}$. Then the Lie equivalence of $e$ is a Lie equivalence of $x$ and $x_{1}$.

AlgHom.toLieHomdefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

the Lie homomorphism of f (from the name)

English

Let $f$ be an algebra homomorphism of $A$ and $B$. Then the Lie homomorphism of $f$ is a Lie homomorphism of $A$ and $B$.

LieAlgebra.addefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\operatorname{ad}$ applied to $R$ and $L$ is a Lie homomorphism of $L$ and the set of ends of $R$ and $L$ defined as the end of $L$ and $L$.

LieModule.IsFaithfulclassMathlib.Algebra.Lie.OfAssociative, predicate

Wording

R is faithful (from the docstring)

English

Let $R$, $L$ and $M$ be sets. Then we can say that $R$ is faithful.

LieModule.toEnddefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

the end of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the end of $L$ and $M$ is a Lie homomorphism of $L$ and the set of ends of $R$ and $M$.

LinearEquiv.lieConjdefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

the Lie conjugate of e (from the name)

English

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

lieSubalgebraOfSubalgebradefMathlib.Algebra.Lie.OfAssociative, function or constant

Wording

the Lie subalgebra of #3 (from the name)

English

Let $R$ and $A$ be sets. Let $\mathrm{A'}$ be a subalgebra of $R$ and $A$. Then the Lie subalgebra of $\mathrm{A'}$ is a Lie subalgebra of $R$ and $A$.

Mathlib.Algebra.Lie.Prod

LieEquiv.prodCommdefMathlib.Algebra.Lie.Prod, function or constant

Wording

no wording

English

Let $R$, $x$ and $x_{1}$ be sets. Then $\operatorname{prodComm}$ applied to $R$, $x$ and $x_{1}$ is a Lie equivalence of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{1}$ and $x$.

LieHom.fstdefMathlib.Algebra.Lie.Prod, function or constant

Wording

the first component of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the first component of $x$ and $x_{1}$ is a Lie homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x$.

LieHom.inldefMathlib.Algebra.Lie.Prod, function or constant

Wording

the left injection of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the left injection of $x$ and $x_{1}$ is a Lie homomorphism of $x$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

LieHom.inrdefMathlib.Algebra.Lie.Prod, function or constant

Wording

the right injection of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the right injection of $x$ and $x_{1}$ is a Lie homomorphism of $x_{1}$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

LieHom.proddefMathlib.Algebra.Lie.Prod, function or constant

Wording

the product of f and g (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $x$. Let $g$ be a Lie homomorphism of $L$ and $x_{1}$. Then the product of $f$ and $g$ is a Lie homomorphism of $L$ and $\mathrm{Prod}$ applied to $x$ and $x_{1}$.

LieHom.prodMapdefMathlib.Algebra.Lie.Prod, function or constant

Wording

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

English

Let $f$ be a Lie homomorphism of $x$ and $x_{2}$. Let $g$ be a Lie homomorphism of $x_{1}$ and $x_{3}$. Then the product map of $f$ and $g$ is a Lie homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $\mathrm{Prod}$ applied to $x_{2}$ and $x_{3}$ defined as the product of the composition of $f$ and the first component of $x$ and $x_{1}$ and the composition of $g$ and the second component of $x$ and $x_{1}$.

LieHom.snddefMathlib.Algebra.Lie.Prod, function or constant

Wording

the second component of x and x1 (from the name)

English

Let $R$, $x$ and $x_{1}$ be sets. Then the second component of $x$ and $x_{1}$ is a Lie homomorphism of $\mathrm{Prod}$ applied to $x$ and $x_{1}$ and $x_{1}$.

Mathlib.Algebra.Lie.Quotient

LieHom.quotKerEquivRangedefMathlib.Algebra.Lie.Quotient, function or constant

Wording

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

English

Let $f$ be a Lie homomorphism of $L$ and $\mathrm{L'}$. Then the quotient kernel equivalence range of $f$ is a Lie equivalence of the set of quotients of $L$ and the kernel of $f$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{5}})}$.

LieIdeal.mkQdefMathlib.Algebra.Lie.Quotient, function or constant

Wording

no wording

English

Let $I$ be a Lie ideal of $R$ and $L$. Then $\operatorname{mkQ}$ applied to $I$ is a Lie homomorphism of $L$ and the set of quotients of $L$ and $I$.

LieSubmodule.Quotient.actionAsEndoMapdefMathlib.Algebra.Lie.Quotient, function or constant

Wording

the action as endomorphism map of N (from the name)

English

Let $N$ be a Lie submodule of $L$ and $M$. Then the action as endomorphism map of $N$ is a Lie homomorphism of $L$ and the set of ends of $R$ and the set of quotients of $M$ and $N$.

LieSubmodule.Quotient.lieSubmoduleInvariantdefMathlib.Algebra.Lie.Quotient, function or constant

Wording

the Lie submodule invariant (from the name)

English

The Lie submodule invariant is a linear map of $L$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{compatibleMaps} (\operatorname{toSubmodule} (N), \operatorname{toSubmodule} (N))}{x_{6}})}$ defined as $\operatorname{codRestrict}$ applied to the compatible map of $\operatorname{toSubmodule}$ applied to $N$ and $\operatorname{toSubmodule}$ applied to $N$, $\operatorname{toLinearMap}$ applied to the end of $L$ and $M$ and the function that maps $x_{6}$ and $x_{7}$ to $\mathrm{LieSubmodule\_\_lie\_mem}$ applied to $N$.

LieSubmodule.Quotient.mkdefMathlib.Algebra.Lie.Quotient, function or constant

Wording

no wording

English

Let $x_{5}$ be an element of $M$. Then $\operatorname{mk}$ applied to $x_{5}$ is a quotient of $M$ and $N$ defined as $\operatorname{mk}$ applied to $x_{5}$.

LieSubmodule.Quotient.mk'defMathlib.Algebra.Lie.Quotient, function or constant

Wording

no wording

English

Let $N$ be a Lie submodule of $L$ and $M$. Then $\operatorname{mk'}$ applied to $N$ is a Lie module homomorphism of $M$ and the set of quotients of $M$ and $N$.

Mathlib.Algebra.Lie.Rank

LieAlgebra.IsRegulardefMathlib.Algebra.Lie.Rank, predicate

Wording

x3 is a regular (from the name)

English

Let $R$ be a set. Let $x_{3}$ be an element of $L$. Then $x_{3}$ is a regular, if $x_{3}$ is a regular.

LieAlgebra.rankdefMathlib.Algebra.Lie.Rank, function or constant

Wording

the rank of R and L (from the name)

English

Let $R$ and $L$ be sets. Then the rank of $R$ and $L$ is a natural number defined as the rank of $L$ and $L$.

LieModule.IsRegulardefMathlib.Algebra.Lie.Rank, predicate

Wording

x6 is a regular (from the name)

English

Let $R$ and $M$ be sets. Let $x_{6}$ be an element of $L$. Then $x_{6}$ is a regular, if $\operatorname{IsNilRegular}$ holds for $\operatorname{toLinearMap}$ applied to the end of $L$ and $M$ and $x_{6}$.

LieModule.rankdefMathlib.Algebra.Lie.Rank, function or constant

Wording

the rank of L and M (from the name)

English

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

Mathlib.Algebra.Lie.SemiDirect

LieAlgebra.SemiDirectSumstructureMathlib.Algebra.Lie.SemiDirect, type

Wording

semi direct sum of L and x5 (from the name)

English

Let $K$ and $L$ be sets. Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then the semi direct sums of $L$ and $x_{5}$ are a basic type.

LieAlgebra.SemiDirectSum.inldefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the left injection of x5 (from the name)

English

Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then the left injection of $x_{5}$ is a Lie homomorphism of $K$ and the set of semi direct sums of $L$ and $x_{5}$.

LieAlgebra.SemiDirectSum.inrdefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the right injection of x5 (from the name)

English

Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then the right injection of $x_{5}$ is a Lie homomorphism of $L$ and the set of semi direct sums of $L$ and $x_{5}$.

LieAlgebra.SemiDirectSum.leftdefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the left of self (from the name)

English

Let $\mathrm{self}$ be a semi direct sum of $L$ and $x_{5}$. Then the left of $\mathrm{self}$ is an element of $K$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

LieAlgebra.SemiDirectSum.prod_isodefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the product isomorphism of K and L (from the name)

English

Let $R$, $K$ and $L$ be sets. Then the product isomorphism of $K$ and $L$ is a Lie equivalence of the set of semi direct sums of $L$ and $0$ and $\mathrm{Prod}$ applied to $K$ and $L$.

LieAlgebra.SemiDirectSum.projldefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

no wording

English

Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then $\operatorname{projl}$ applied to $x_{5}$ is a linear map of the set of semi direct sums of $L$ and $x_{5}$ and $K$.

LieAlgebra.SemiDirectSum.projrdefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

no wording

English

Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then $\operatorname{projr}$ applied to $x_{5}$ is a Lie homomorphism of the set of semi direct sums of $L$ and $x_{5}$ and $L$.

LieAlgebra.SemiDirectSum.rightdefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the right of self (from the name)

English

Let $\mathrm{self}$ be a semi direct sum of $L$ and $x_{5}$. Then the right of $\mathrm{self}$ is an element of $L$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$.

LieAlgebra.SemiDirectSum.toProddefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

the product (from the name)

English

The product is an equivalence from the set of semi direct sums of $L$ and $x_{5}$ to $\mathrm{Prod}$ applied to $K$ and $L$.

LieAlgebra.SemiDirectSum.toProdldefMathlib.Algebra.Lie.SemiDirect, function or constant

Wording

no wording

English

Let $x_{5}$ be a Lie homomorphism of $L$ and the set of Lie derivations of $K$ and $K$. Then $\operatorname{toProdl}$ applied to $x_{5}$ is a linear equivalence of the set of semi direct sums of $L$ and $x_{5}$ and $\mathrm{Prod}$ applied to $K$ and $L$.

Mathlib.Algebra.Lie.Semisimple.Defs

LieAlgebra.HasCentralRadicalclassMathlib.Algebra.Lie.Semisimple.Defs, predicate

Wording

no wording

English

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

LieAlgebra.HasTrivialRadicalclassMathlib.Algebra.Lie.Semisimple.Defs, predicate

Wording

no wording

English

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

LieAlgebra.IsSemisimpleclassMathlib.Algebra.Lie.Semisimple.Defs, predicate

Wording

no wording

English

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

LieAlgebra.IsSimpleclassMathlib.Algebra.Lie.Semisimple.Defs, predicate

Wording

R is simple (from the docstring)

English

Let $R$ and $L$ be sets. Then we can say that $R$ is simple.

LieModule.IsIrreducibledefMathlib.Algebra.Lie.Semisimple.Defs, predicate

Wording

R is irreducible (from the docstring)

English

Let $R$, $L$ and $M$ be sets. Then $R$ is irreducible, if the set of Lie submodules of $L$ and $M$ is a simple order.

Mathlib.Algebra.Lie.SerreConstruction

CartanMatrix.GeneratorsinductiveMathlib.Algebra.Lie.SerreConstruction, type

Wording

generator of B (from the name)

English

Let $B$ be a set. Then the generators of $B$ are a basic type.

CartanMatrix.Generators.EconstructorMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $x$ be an element of $B$. Then $\operatorname{E}$ applied to $x$ is a generator of $B$.

CartanMatrix.Generators.FconstructorMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $x$ be an element of $B$. Then $\operatorname{F}$ applied to $x$ is a generator of $B$.

CartanMatrix.Generators.HconstructorMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $x$ be an element of $B$. Then $\operatorname{H}$ applied to $x$ is a generator of $B$.

CartanMatrix.Generators.ctorElimTypedefMathlib.Algebra.Lie.SerreConstruction, 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 $B$ to elements of $\mathrm{motive}$ applied to $\operatorname{H}$ applied to $x$ and $\mathrm{cond}$ applied to $\operatorname{ble}$ applied to $\mathrm{ctorIdx}$ and $1$, $\mathrm{PULift}$ applied to the set of functions from elements $x_{1}$ of $B$ to elements of $\mathrm{motive}$ applied to $\operatorname{E}$ applied to $x_{1}$ and $\mathrm{PULift}$ applied to the set of functions from elements $x_{2}$ of $B$ to elements of $\mathrm{motive}$ applied to $\operatorname{F}$ applied to $x_{2}$.

CartanMatrix.Relations.EFdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{2}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{EF}$ applied to $R$ and $x_{2}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to $\iteMACRoG {(\EqtMACRoH {i}{j})}{(\operatorname{bracket} (\operatorname{comp} (\operatorname{of} (R), \operatorname{E} , i), \operatorname{comp} (\operatorname{of} (R), \operatorname{F} , i))- \operatorname{comp} (\operatorname{of} (R), \operatorname{H} , i))}{\operatorname{bracket} (\operatorname{comp} (\operatorname{of} (R), \operatorname{E} , i), \operatorname{comp} (\operatorname{of} (R), \operatorname{F} , j))}$ and $x_{2}$.

CartanMatrix.Relations.HEdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{HE}$ applied to $R$, $\mathrm{CM}$ and $x_{1}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to the difference between the bracket of $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{H}$ and $i$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{E}$ and $j$ and $\HSMulhSMulMACRoAL {\mathrm{CM} (i , j)}{\operatorname{comp} (\operatorname{of} (R), \operatorname{E} , j)}$ and $x_{1}$.

CartanMatrix.Relations.HFdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{HF}$ applied to $R$, $\mathrm{CM}$ and $x_{1}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to the sum of the bracket of $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{H}$ and $i$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{F}$ and $j$ and $\HSMulhSMulMACRoAL {\mathrm{CM} (i , j)}{\operatorname{comp} (\operatorname{of} (R), \operatorname{F} , j)}$ and $x_{1}$.

CartanMatrix.Relations.HHdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{HH}$ applied to $R$ and $x_{1}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to the bracket of $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{H}$ and $i$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{H}$ and $j$ and $x_{1}$.

CartanMatrix.Relations.adEdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{adE}$ applied to $R$, $\mathrm{CM}$ and $x_{1}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to $\operatorname{hPow}$ applied to $\operatorname{ad}$ applied to $R$, the set of free Lie algebras of $R$ and the set of generators of $B$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{E}$ and $i$, $\operatorname{toNat}$ applied to $\operatorname{neg}$ applied to $\mathrm{CM}$ applied to $i$ and $j$ and the bracket of $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{E}$ and $i$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{E}$ and $j$ and $x_{1}$.

CartanMatrix.Relations.adFdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

no wording

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Let $x_{1}$ be an element of $\mathrm{Prod}$ applied to $B$ and $B$. Then $\operatorname{adF}$ applied to $R$, $\mathrm{CM}$ and $x_{1}$ is a free Lie algebra of $R$ and the set of generators of $B$ defined as $\operatorname{uncurry}$ applied to the function that maps $i$ and $j$ to $\operatorname{hPow}$ applied to $\operatorname{ad}$ applied to $R$, the set of free Lie algebras of $R$ and the set of generators of $B$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{F}$ and $i$, $\operatorname{toNat}$ applied to $\operatorname{neg}$ applied to $\mathrm{CM}$ applied to $i$ and $j$ and the bracket of $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{F}$ and $i$ and $\operatorname{comp}$ applied to $\operatorname{of}$ applied to $R$, $\operatorname{F}$ and $j$ and $x_{1}$.

CartanMatrix.Relations.toIdealdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

the ideal of the free Lie algebra generated by the relations of R and CM (from the docstring)

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Then the ideal of the free Lie algebra generated by the relations of $R$ and $\mathrm{CM}$ is a Lie ideal of $R$ and the set of free Lie algebras of $R$ and the set of generators of $B$ defined as the Lie span of the set of $R$ and $\mathrm{CM}$.

CartanMatrix.Relations.toSetdefMathlib.Algebra.Lie.SerreConstruction, function or constant

Wording

the set of R and CM (from the name)

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Then the set of $R$ and $\mathrm{CM}$ is an element of the power set of the set of free Lie algebras of $R$ and the set of generators of $B$ defined as the union of the union of the union of the union of the union of the range of $\operatorname{HH}$ applied to $R$ and the range of $\operatorname{EF}$ applied to $R$ and the range of $\operatorname{HE}$ applied to $R$ and $\mathrm{CM}$ and the range of $\operatorname{HF}$ applied to $R$ and $\mathrm{CM}$ and the range of $\operatorname{adE}$ applied to $R$ and $\mathrm{CM}$ and the range of $\operatorname{adF}$ applied to $R$ and $\mathrm{CM}$.

CartanMatrix.aₙdefMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then an element of $\mathrm{CartanMatrix\_\_a\_u2099\_}$ applied to $R$ and $n$ is an element of the function that maps $R$ and $n$ to the set of Lie algebras of $R$ and $\operatorname{A}$ applied to $n$.

CartanMatrix.bₙdefMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then an element of $\mathrm{CartanMatrix\_\_b\_u2099\_}$ applied to $R$ and $n$ is an element of the function that maps $R$ and $n$ to the set of Lie algebras of $R$ and $\operatorname{B}$ applied to $n$.

CartanMatrix.cₙdefMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then an element of $\mathrm{CartanMatrix\_\_c\_u2099\_}$ applied to $R$ and $n$ is an element of the function that maps $R$ and $n$ to the set of Lie algebras of $R$ and $\operatorname{C}$ applied to $n$.

CartanMatrix.dₙdefMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Let $n$ be a natural number. Then an element of $\mathrm{CartanMatrix\_\_d\_u2099\_}$ applied to $R$ and $n$ is an element of the function that maps $R$ and $n$ to the set of Lie algebras of $R$ and $\operatorname{D}$ applied to $n$.

LieAlgebra.e₆defMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\mathrm{LieAlgebra\_\_e\_u2086\_}$ applied to $R$ is an element of the function that maps $R$ to the set of Lie algebras of $R$ and $\operatorname{E}$ applied to $6$.

LieAlgebra.e₇defMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\mathrm{LieAlgebra\_\_e\_u2087\_}$ applied to $R$ is an element of the function that maps $R$ to the set of Lie algebras of $R$ and $\operatorname{E}$ applied to $7$.

LieAlgebra.e₈defMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\mathrm{LieAlgebra\_\_e\_u2088\_}$ applied to $R$ is an element of the function that maps $R$ to the set of Lie algebras of $R$ and $\operatorname{E}$ applied to $8$.

LieAlgebra.f₄defMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\mathrm{LieAlgebra\_\_f\_u2084\_}$ applied to $R$ is an element of the function that maps $R$ to the set of Lie algebras of $R$ and $\mathrm{CartanMatrix\_\_F\_u2084\_}$.

LieAlgebra.g₂defMathlib.Algebra.Lie.SerreConstruction, type

Wording

no wording

English

Let $R$ be a set. Then an element of $\mathrm{LieAlgebra\_\_g\_u2082\_}$ applied to $R$ is an element of the function that maps $R$ to the set of Lie algebras of $R$ and $\mathrm{CartanMatrix\_\_G\_u2082\_}$.

Matrix.ToLieAlgebradefMathlib.Algebra.Lie.SerreConstruction, type

Wording

Lie algebra of R and CM (from the name)

English

Let $R$ be a set. Let $\mathrm{CM}$ be a matrix of $B$ and $\Integer$. Then a Lie algebra of $R$ and $\mathrm{CM}$ is an element of the function that maps $R$ and $\mathrm{CM}$ to the set of quotients of the set of free Lie algebras of $R$ and the set of generators of $B$ and the ideal of the free Lie algebra generated by the relations of $R$ and $\mathrm{CM}$.

Mathlib.Algebra.Lie.SkewAdjoint

skewAdjointLieSubalgebradefMathlib.Algebra.Lie.SkewAdjoint, function or constant

Wording

the skew adjoint Lie subalgebra of B (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Then the skew adjoint Lie subalgebra of $B$ is a Lie subalgebra of $R$ and the set of ends of $R$ and $M$ defined as $\operatorname{mk}$ applied to the skew adjoint submodule of $B$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{LinearMap\_\_BilinForm\_\_isSkewAdjoint\_bracket}$ applied to $B$.

skewAdjointLieSubalgebraEquivdefMathlib.Algebra.Lie.SkewAdjoint, function or constant

Wording

the skew adjoint Lie subalgebra equivalence of B and e (from the name)

English

Let $B$ be a bilinear form of $R$ and $M$. Let $e$ be a linear equivalence of $N$ and $M$. Then the skew adjoint Lie subalgebra equivalence of $B$ and $e$ is a Lie equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{skewAdjointLieSubalgebra} (\mathrm{LinearMap\_\_compl\_u2081\_\_u2082\_} (\operatorname{toLinearMap} (e), \operatorname{toLinearMap} (e)))}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{skewAdjointLieSubalgebra} (B)}{x_{6}})}$.

skewAdjointMatricesLieSubalgebradefMathlib.Algebra.Lie.SkewAdjoint, function or constant

Wording

the skew adjoint matrice Lie subalgebra of J (from the name)

English

Let $J$ be a matrix of $n$ and $R$. Then the skew adjoint matrice Lie subalgebra of $J$ is a Lie subalgebra of $R$ and the set of matrixes of $n$ and $R$ defined as $\operatorname{mk}$ applied to the skew adjoint matrice submodule of $J$ and the function that maps $x_{3}$ and $x_{4}$ to $\mathrm{Matrix\_\_isSkewAdjoint\_bracket}$ applied to $J$.

skewAdjointMatricesLieSubalgebraEquivdefMathlib.Algebra.Lie.SkewAdjoint, function or constant

Wording

the skew adjoint matrice Lie subalgebra equivalence of J and P (from the name)

English

Let $J$ and $P$ be matrixes of $n$ and $R$ such that $P$ is invertible. Then the skew adjoint matrice Lie subalgebra equivalence of $J$ and $P$ is a Lie equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{skewAdjointMatricesLieSubalgebra} (J)}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{skewAdjointMatricesLieSubalgebra} (\operatorname{transpose} (P)\times J \times P)}{x_{4}})}$.

skewAdjointMatricesLieSubalgebraEquivTransposedefMathlib.Algebra.Lie.SkewAdjoint, function or constant

Wording

the skew adjoint matrice Lie subalgebra equivalence transpose of J and e (from the name)

English

Let $J$ be a matrix of $n$ and $R$. Let $e$ be an algebra isomorphism of the set of matrixes of $n$ and $R$ and the set of matrixes of $m$ and $R$ such that for all matrixes $A$ of $n$ and $R$, $\EqtMACRoH {\operatorname{transpose} (e (A))}{e (\operatorname{transpose} (A))}$. Then the skew adjoint matrice Lie subalgebra equivalence transpose of $J$ and $e$ is a Lie equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\mathrm{skewAdjointMatricesLieSubalgebra} (J)}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{skewAdjointMatricesLieSubalgebra} (e (J))}{x_{6}})}$.

Mathlib.Algebra.Lie.Sl2

IsSl2TriplestructureMathlib.Algebra.Lie.Sl2, predicate

Wording

no wording

English

Let $h$, $e$ and $f$ be elements of $L$. Then we can say that $\mathrm{IsSl2Triple}$ holds for $h$, $e$ and $f$.

IsSl2Triple.HasPrimitiveVectorWithstructureMathlib.Algebra.Lie.Sl2, predicate

Wording

no wording

English

Assume that $\mathrm{IsSl2Triple}$ holds for $h$, $e$ and $f$. Let $m$ be an element of $M$. Let $x_{5}$ be an element of $R$. Then we can say that $\operatorname{HasPrimitiveVectorWith}$ holds for $t$, $m$ and $x_{5}$.

IsSl2Triple.toLieSubalgebradefMathlib.Algebra.Lie.Sl2, function or constant

Wording

the Lie subalgebra of R and t (from the name)

English

Let $R$ be a set. Assume that $\mathrm{IsSl2Triple}$ holds for $h$, $e$ and $f$. Then the Lie subalgebra of $R$ and $t$ is a Lie subalgebra of $R$ and $L$.

Mathlib.Algebra.Lie.Solvable

LieAlgebra.IsSolvableclassMathlib.Algebra.Lie.Solvable, predicate

Wording

L is solvable (from the docstring)

English

Let $L$ be a set. Then we can say that $L$ is solvable.

LieAlgebra.derivedAbelianOfIdealdefMathlib.Algebra.Lie.Solvable, function or constant

Wording

no wording

English

Let $I$ be a Lie ideal of $R$ and $L$. Then $\operatorname{derivedAbelianOfIdeal}$ applied to $I$ is a Lie ideal of $R$ and $L$.

LieAlgebra.derivedLengthdefMathlib.Algebra.Lie.Solvable, function or constant

Wording

the derived length of R and L (from the docstring)

English

Let $R$ and $L$ be sets. Then the derived length of $R$ and $L$ is a natural number defined as the derived length of the top.

LieAlgebra.derivedLengthOfIdealdefMathlib.Algebra.Lie.Solvable, function or constant

Wording

the derived length of I (from the name)

English

Let $R$ and $L$ be sets. Let $I$ be a Lie ideal of $R$ and $L$. Then the derived length of $I$ is a natural number defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $k$ to the proposition that the derived series of $k$ and $I$ is equal to the bottom.

LieAlgebra.derivedSeriesdefMathlib.Algebra.Lie.Solvable, function or constant

Wording

the derived series of k (from the name)

English

Let $R$ and $L$ be sets. Let $k$ be a natural number. Then the derived series of $k$ is a Lie ideal of $R$ and $L$ defined as the derived series of $k$ and the top.

LieAlgebra.derivedSeriesOfIdealdefMathlib.Algebra.Lie.Solvable, function or constant

Wording

the derived series of k and x3 (from the name)

English

Let $R$ and $L$ be sets. Let $k$ be a natural number. Let $x_{3}$ be a Lie ideal of $R$ and $L$. Then the derived series of $k$ and $x_{3}$ is a Lie ideal of $R$ and $L$ defined as $\operatorname{iterate}$ applied to the function that maps $I$ to the bracket of $I$ and $I$, $k$ and $x_{3}$.

LieAlgebra.radicaldefMathlib.Algebra.Lie.Solvable, function or constant

Wording

the radical of R and L (from the name)

English

Let $R$ and $L$ be sets. Then the radical of $R$ and $L$ is a Lie ideal of $R$ and $L$ defined as the supremum of $\operatorname{ofPred}$ applied to the function that maps $I$ to the proposition that $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {I}{x_{3}})}$ is solvable.

Mathlib.Algebra.Lie.Subalgebra

LieEquiv.lieSubalgebraMapdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the Lie subalgebra map of x7 and e (from the name)

English

Let $x_{7}$ be a Lie subalgebra of $R$ and $x$. Let $e$ be a Lie equivalence of $x$ and $x_{1}$. Then the Lie subalgebra map of $x_{7}$ and $e$ is a Lie equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {x_{7}}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{map} (\operatorname{toLieHom} (e), x_{7})}{x_{9}})}$.

LieEquiv.ofEqdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

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

English

Let $x_{4}$ and $x_{5}$ be Lie subalgebras of $R$ and $x$ such that $\EqtMACRoH {x_{4}}{x_{5}}$. Then the Lie equivalence of $x_{4}$ and $x_{5}$ is a Lie equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {x_{4}}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {x_{5}}{x_{7}})}$.

LieEquiv.ofInjectivedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the Lie equivalence of f and h (from the name)

English

Let $f$ be a Lie homomorphism of $x$ and $x_{1}$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the Lie equivalence of $f$ and $h$ is a Lie equivalence of $x$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{7}})}$.

LieEquiv.ofSubalgebrasdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the Lie equivalence of x8 and e (from the name)

English

Let $x_{7}$ be a Lie subalgebra of $R$ and $x$. Let $x_{8}$ be a Lie subalgebra of $R$ and $x_{1}$. Let $e$ be a Lie equivalence of $x$ and $x_{1}$ such that the map of $\operatorname{toLieHom}$ applied to $e$ and $x_{7}$ is equal to $x_{8}$. Then the Lie equivalence of $x_{8}$ and $e$ is a Lie equivalence of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {x_{7}}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {x_{8}}{x_{10}})}$.

LieHom.equivRangeOfInjectivedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the equivalence range of f and h (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$ such that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence range of $f$ and $h$ is a Lie equivalence of $L$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{6}})}$.

LieHom.rangedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Then the range of $f$ is a Lie subalgebra of $R$ and $x_{3}$.

LieHom.rangeRestrictdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

no wording

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Then $\operatorname{rangeRestrict}$ applied to $f$ is a Lie homomorphism of $L$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\operatorname{range} (f)}{x_{6}})}$.

LieModuleHom.restrictLiedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

no wording

English

Let $f$ be a Lie module homomorphism of $M$ and $N$. Let $\mathrm{L'}$ be a Lie subalgebra of $R$ and $L$. Then $\operatorname{restrictLie}$ applied to $f$ and $\mathrm{L'}$ is a Lie module homomorphism of $M$ and $N$.

LieSubalgebrastructureMathlib.Algebra.Lie.Subalgebra, type

Wording

Lie subalgebra of R and L (from the name)

English

Let $R$ and $L$ be sets. Then the Lie subalgebras of $R$ and $L$ are a basic type.

LieSubalgebra.comapdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the preimage of f and x6 (from the docstring)

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Let $x_{6}$ be a Lie subalgebra of $R$ and $x_{3}$. Then the preimage of $f$ and $x_{6}$ is a Lie subalgebra of $R$ and $L$.

LieSubalgebra.equivMapOfInjectivedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

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

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Let $K$ be a Lie subalgebra of $R$ and $L$. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $f$ and $K$ is a Lie equivalence of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {K}{x_{6}})}$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{map} (f , K)}{x_{7}})}$.

LieSubalgebra.equivOfLedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the equivalence of h (from the name)

English

Assume that $K \leq \mathrm{K'}$. Then the equivalence of $h$ is a Lie equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {K}{x_{3}})}$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\operatorname{ofLe} (h)}{x_{4}})}$ defined as the equivalence range of the inclusion of $h$ and $\mathrm{LieSubalgebra\_\_inclusion\_injective}$ applied to $h$.

LieSubalgebra.gidefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\operatorname{gi}$ applied to $R$ and $L$ is a Galois insertion of $\operatorname{lieSpan}$ and $\operatorname{instSetLike}$ applied to $R$ and $L$.

LieSubalgebra.incldefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the inclusion of #1 (from the name)

English

Let $\mathrm{L'}$ be a Lie subalgebra of $R$ and $L$. Then the inclusion of $\mathrm{L'}$ is a Lie homomorphism of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{L'}}{x_{3}})}$ and $L$.

LieSubalgebra.incl'defMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the inclusion of #1 (from the name)

English

Let $\mathrm{L'}$ be a Lie subalgebra of $R$ and $L$. Then the inclusion of $\mathrm{L'}$ is a Lie module homomorphism of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {\mathrm{L'}}{x_{4}})}$ and $L$.

LieSubalgebra.inclusiondefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the inclusion of h (from the name)

English

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

LieSubalgebra.lieSpandefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the Lie span of s (from the name)

English

Let $R$ and $L$ be sets. Let $s$ be an element of $\wp L$. Then the Lie span of $s$ is a Lie subalgebra of $R$ and $L$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $N$ to $\mathrm{Leq} (s , N)$.

LieSubalgebra.mapdefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the map of f and K (from the name)

English

Let $f$ be a Lie homomorphism of $L$ and $x_{3}$. Let $K$ be a Lie subalgebra of $R$ and $L$. Then the map of $f$ and $K$ is a Lie subalgebra of $R$ and $x_{3}$.

LieSubalgebra.ofLedefMathlib.Algebra.Lie.Subalgebra, function or constant

Wording

the Lie subalgebra of h (from the name)

English

Assume that $K \leq \mathrm{K'}$. Then the Lie subalgebra of $h$ is a Lie subalgebra of $R$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\mathrm{K'}}{x_{3}})}$ defined as the range of the inclusion of $h$.

Mathlib.Algebra.Lie.Submodule

LieModuleEquiv.ofTopdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the Lie module equivalence of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the Lie module equivalence of $L$ and $M$ is a Lie module equivalence of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{5}})}$ and $M$.

LieModuleHom.codRestrictdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

no wording

English

Let $P$ be a Lie submodule of $L$ and $N$. Let $f$ be a Lie module homomorphism of $M$ and $N$ such that for all elements $m$ of $M$, $\MembershipmemMACRoT {P}{f (m)}$. Then $\operatorname{codRestrict}$ applied to $P$, $f$ and $h$ is a Lie module homomorphism of $M$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {P}{x_{8}})}$.

LieModuleHom.kerdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a Lie module homomorphism of $M$ and $N$. Then the kernel of $f$ is a Lie submodule of $L$ and $M$ defined as the preimage of $f$ and the bottom.

LieModuleHom.rangedefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the range of f (from the docstring)

English

Let $f$ be a Lie module homomorphism of $M$ and $N$. Then the range of $f$ is a Lie submodule of $L$ and $N$.

LieSubalgebra.toLieSubmoduledefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the Lie submodule of K (from the name)

English

Let $K$ be a Lie subalgebra of $R$ and $L$. Then the Lie submodule of $K$ is a Lie submodule of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {K}{x_{3}})}$ and $L$.

LieSubalgebra.topEquivdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the top equivalence (from the name)

English

The top equivalence is a Lie equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{top}}{x_{3}})}$ and $L$.

LieSubmodulestructureMathlib.Algebra.Lie.Submodule, type

Wording

Lie submodule of L and M (from the name)

English

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

LieSubmodule.comapdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the preimage of f and #2 (from the name)

English

Let $f$ be a Lie module homomorphism of $M$ and $\mathrm{M'}$. Let $\mathrm{N'}$ be a Lie submodule of $L$ and $\mathrm{M'}$. Then the preimage of $f$ and $\mathrm{N'}$ is a Lie submodule of $L$ and $M$.

LieSubmodule.copydefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the copy of N and s (from the name)

English

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

LieSubmodule.equivMapOfInjectivedefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the equivalence map of N and hf (from the name)

English

Let $N$ be a Lie submodule of $L$ and $M$. Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the equivalence map of $N$ and $\mathrm{hf}$ is a Lie module equivalence of $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {N}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{map} (f , N)}{x_{9}})}$.

LieSubmodule.gidefMathlib.Algebra.Lie.Submodule, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Then $\operatorname{gi}$ applied to $R$, $L$ and $M$ is a Galois insertion of $\operatorname{lieSpan}$ and $\operatorname{instSetLike}$.

LieSubmodule.incldefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the inclusion of N (from the docstring)

English

Let $N$ be a Lie submodule of $L$ and $M$. Then the inclusion of $N$ is a Lie module homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$ and $M$.

LieSubmodule.inclusiondefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the inclusion of h (from the name)

English

Assume that $N \leq \mathrm{N'}$. Then the inclusion of $h$ is a Lie module homomorphism of $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {N}{x_{5}})}$ and $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{6}})}$.

LieSubmodule.lieSpandefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the Lie span of s (from the name)

English

Let $R$ and $L$ be sets. Let $s$ be an element of $\wp M$. Then the Lie span of $s$ is a Lie submodule of $L$ and $M$ defined as the infimum of $\operatorname{ofPred}$ applied to the function that maps $N$ to $\mathrm{Leq} (s , N)$.

LieSubmodule.mapdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the map of f and N (from the name)

English

Let $f$ be a Lie module homomorphism of $M$ and $\mathrm{M'}$. Let $N$ be a Lie submodule of $L$ and $M$. Then the map of $f$ and $N$ is a Lie submodule of $L$ and $\mathrm{M'}$.

LieSubmodule.mapOrderEmbeddingdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the map order embedding of hf (from the name)

English

Assume that $\operatorname{coe}$ applied to $f$ is injective. Then the map order embedding of $\mathrm{hf}$ is an order embedding of the set of Lie submodules of $L$ and $M$ and the set of Lie submodules of $L$ and $\mathrm{M'}$.

LieSubmodule.orderIsoMapComapdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

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

English

Let $e$ be a Lie module equivalence of $M$ and $\mathrm{M'}$. Then the order isomorphism map preimage of $e$ is an order isomorphism of the set of Lie submodules of $L$ and $M$ and the set of Lie submodules of $L$ and $\mathrm{M'}$.

LieSubmodule.restrdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the restriction of N and H (from the name)

English

Let $N$ be a Lie submodule of $L$ and $M$. Let $H$ be a Lie subalgebra of $R$ and $L$. Then the restriction of $N$ and $H$ is a Lie submodule of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {H}{x_{6}})}$ and $M$.

LieSubmodule.toSubmodule_orderEmbeddingdefMathlib.Algebra.Lie.Submodule, function or constant

Wording

the submodule order embedding of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the submodule order embedding of $L$ and $M$ is an order embedding of the set of Lie submodules of $L$ and $M$ and the set of submodules of $R$ and $M$.

Mathlib.Algebra.Lie.TensorProduct

LieModule.toModuleHomdefMathlib.Algebra.Lie.TensorProduct, function or constant

Wording

the module homomorphism of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the module homomorphism of $L$ and $M$ is a Lie module homomorphism of the set of tensor products of $L$ and $M$ and $M$.

TensorProduct.LieModule.liftdefMathlib.Algebra.Lie.TensorProduct, function or constant

Wording

the lift of N and P (from the name)

English

Let $R$, $L$, $M$, $N$ and $P$ be sets. Then the lift of $N$ and $P$ is a Lie module equivalence of the set of linear maps of $M$ and the set of linear maps of $N$ and $P$ and the set of linear maps of the set of tensor products of $M$ and $N$ and $P$.

TensorProduct.LieModule.liftLiedefMathlib.Algebra.Lie.TensorProduct, function or constant

Wording

no wording

English

Let $R$, $L$, $M$, $N$ and $P$ be sets. Then $\operatorname{liftLie}$ applied to $R$, $L$, $M$, $N$ and $P$ is a linear equivalence of the set of Lie module homomorphisms of $M$ and the set of linear maps of $N$ and $P$ and the set of Lie module homomorphisms of the set of tensor products of $M$ and $N$ and $P$ defined as the composition of the composition of the inverse of the maximum trivial linear map equivalence Lie module homomorphism and the linear equivalence of the maximum trivial equivalence of the lift of $N$ and $P$ and the maximum trivial linear map equivalence Lie module homomorphism.

TensorProduct.LieModule.mapdefMathlib.Algebra.Lie.TensorProduct, function or constant

Wording

the map of f and g (from the name)

English

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

TensorProduct.LieModule.mapIncldefMathlib.Algebra.Lie.TensorProduct, function or constant

Wording

the map inclusion of #1 and #2 (from the name)

English

Let $\mathrm{M'}$ be a Lie submodule of $L$ and $M$. Let $\mathrm{N'}$ be a Lie submodule of $L$ and $N$. Then the map inclusion of $\mathrm{M'}$ and $\mathrm{N'}$ is a Lie module homomorphism of the set of tensor products of $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\mathrm{M'}}{x_{9}})}$ and $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\mathrm{N'}}{x_{10}})}$ and the set of tensor products of $M$ and $N$ defined as the map of the inclusion of $\mathrm{M'}$ and the inclusion of $\mathrm{N'}$.

Mathlib.Algebra.Lie.TraceForm

LieIdeal.killingCompldefMathlib.Algebra.Lie.TraceForm, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Let $I$ be a Lie ideal of $R$ and $L$. Then $\operatorname{killingCompl}$ applied to $R$, $L$ and $I$ is a Lie ideal of $R$ and $L$.

LieModule.traceFormdefMathlib.Algebra.Lie.TraceForm, function or constant

Wording

the trace form of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the trace form of $L$ and $M$ is a bilinear form of $R$ and $L$ defined as $\mathrm{LinearMap\_\_compr\_u2082\_}$ applied to the complement of $\operatorname{toLinearMap}$ applied to the end of $L$ and $M$ and $\operatorname{toLinearMap}$ applied to the end of $L$ and $M$ and the trace of $R$ and $M$.

killingFormdefMathlib.Algebra.Lie.TraceForm, function or constant

Wording

no wording

English

Let $R$ and $L$ be sets. Then $\mathrm{killingForm}$ applied to $R$ and $L$ is a bilinear form of $R$ and $L$ defined as the trace form of $L$ and $L$.

Mathlib.Algebra.Lie.TransferInstance

LinearEquiv.lieEquivdefMathlib.Algebra.Lie.TransferInstance, function or constant

Wording

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

English

Let $R$ be a set. Let $e$ be a linear equivalence of $M$ and $L$. Then the Lie equivalence of $R$ and $e$ is a Lie equivalence of $M$ and $L$.

Mathlib.Algebra.Lie.UniversalEnveloping

UniversalEnvelopingAlgebradefMathlib.Algebra.Lie.UniversalEnveloping, type

Wording

universal enveloping algebra of R and L (from the name)

English

Let $R$ and $L$ be sets. Then a universal enveloping algebra of $R$ and $L$ is an element of the function that maps $R$ and $L$ to the set of quotients of the ring congruence relation of $R$ and $L$.

UniversalEnvelopingAlgebra.RelinductiveMathlib.Algebra.Lie.UniversalEnveloping, predicate

Wording

no wording

English

Let $R$ and $L$ be sets. Let $x_{3}$ and $x_{4}$ be tensor algebras of $R$ and $L$. Then we can say that $\operatorname{Rel}$ holds for $R$, $L$, $x_{3}$ and $x_{4}$.

UniversalEnvelopingAlgebra.liftdefMathlib.Algebra.Lie.UniversalEnveloping, function or constant

Wording

the lift of R (from the name)

English

Let $R$ be a set. Then the lift of $R$ is an equivalence from the set of Lie homomorphisms of $L$ and $A$ to the set of algebra homomorphisms of the set of universal enveloping algebras of $R$ and $L$ and $A$.

UniversalEnvelopingAlgebra.mkAlgHomdefMathlib.Algebra.Lie.UniversalEnveloping, function or constant

Wording

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

English

Let $R$ and $L$ be sets. Then the algebra homomorphism of $R$ and $L$ is an algebra homomorphism of the set of tensor algebras of $R$ and $L$ and the set of universal enveloping algebras of $R$ and $L$ defined as $\mathrm{RingCon\_\_mk\_u2090\_}$ applied to $R$ and the ring congruence relation of $R$ and $L$.

UniversalEnvelopingAlgebra.ringCondefMathlib.Algebra.Lie.UniversalEnveloping, function or constant

Wording

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

English

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

UniversalEnvelopingAlgebra.ιdefMathlib.Algebra.Lie.UniversalEnveloping, function or constant

Wording

the inclusion of R (from the name)

English

Let $R$ be a set. Then the inclusion of $R$ is a Lie homomorphism of $L$ and the set of universal enveloping algebras of $R$ and $L$.

Mathlib.Algebra.Lie.Weights.Basic

LieModule.IsTriangularizableclassMathlib.Algebra.Lie.Weights.Basic, predicate

Wording

no wording

English

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

LieModule.WeightstructureMathlib.Algebra.Lie.Weights.Basic, type

Wording

no wording

English

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

LieModule.Weight.IsNonZerodefMathlib.Algebra.Lie.Weights.Basic, predicate

Wording

x6 is non zero (from the name)

English

Let $x_{6}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then $x_{6}$ is non zero, if $x_{6}$ is not zero.

LieModule.Weight.IsZerodefMathlib.Algebra.Lie.Weights.Basic, predicate

Wording

x6 is zero (from the name)

English

Let $x_{6}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then $x_{6}$ is zero, if $\operatorname{coe}$ applied to $x_{6}$ is equal to $0$.

LieModule.Weight.equivSetOfPreddefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

the equivalence set of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the equivalence set of $L$ and $M$ is an equivalence from $\operatorname{Weight}$ applied to $R$, $L$ and $M$ to the set of elements of $\operatorname{ofPred}$ applied to the function that maps $x_{6}$ to the proposition that $\operatorname{genWeightSpace}$ applied to $M$ and $x_{6}$ is distinct from the bottom.

LieModule.Weight.toFundefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Let $x_{6}$ be an element of $L$. Then $\operatorname{toFun}$ applied to $\mathrm{self}$ and $x_{6}$ is an element of $R$ defined as $\operatorname{proj0}$ applied to $\mathrm{self}$ and $x_{6}$.

LieModule.genWeightSpacedefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

no wording

English

Let $M$ be a set. Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Then $\operatorname{genWeightSpace}$ applied to $M$ and $x_{6}$ is a Lie submodule of $L$ and $M$ defined as the infimum of the function that maps $x_{7}$ to $\operatorname{genWeightSpaceOf}$ applied to $M$, $x_{6}$ applied to $x_{7}$ and $x_{7}$.

LieModule.genWeightSpaceOfdefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

no wording

English

Let $M$ be a set. Let $x_{6}$ be an element of $R$. Let $x_{7}$ be an element of $L$. Then $\operatorname{genWeightSpaceOf}$ applied to $M$, $x_{6}$ and $x_{7}$ is a Lie submodule of $L$ and $M$.

LieModule.posFittingCompdefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

the positive part fitting composition of L and M (from the name)

English

Let $R$, $L$ and $M$ be sets. Then the positive part fitting composition of $L$ and $M$ is a Lie submodule of $L$ and $M$ defined as the supremum of the function that maps $x_{6}$ to the positive part fitting composition of $x_{6}$.

LieModule.posFittingCompOfdefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

the positive part fitting composition of x6 (from the name)

English

Let $R$ and $M$ be sets. Let $x_{6}$ be an element of $L$. Then the positive part fitting composition of $x_{6}$ is a Lie submodule of $L$ and $M$.

LieModule.weightSpacedefMathlib.Algebra.Lie.Weights.Basic, function or constant

Wording

no wording

English

Let $M$ be a set. Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Then $\operatorname{weightSpace}$ applied to $M$ and $x_{6}$ is a Lie submodule of $L$ and $M$.

Mathlib.Algebra.Lie.Weights.Cartan

LieAlgebra.corootSpacedefMathlib.Algebra.Lie.Weights.Cartan, function or constant

Wording

the coroot space of x3 (from the name)

English

Let $x_{3}$ be a function from elements of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {H}{x_{6}})}$ to elements of $R$. Then the coroot space of $x_{3}$ is a Lie ideal of $R$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$.

LieAlgebra.rootSpacedefMathlib.Algebra.Lie.Weights.Cartan, function or constant

Wording

the root space of H and x3 (from the name)

English

Let $H$ be a Lie subalgebra of $R$ and $L$. Let $x_{3}$ be a function from elements of $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {H}{x_{6}})}$ to elements of $R$. Then the root space of $H$ and $x_{3}$ is a Lie submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $L$ defined as $\operatorname{genWeightSpace}$ applied to $L$ and $x_{3}$.

LieAlgebra.rootSpaceProductdefMathlib.Algebra.Lie.Weights.Cartan, function or constant

Wording

the root space product of x4 and x5 (from the name)

English

Let $R$ and $L$ be sets. Let $H$ be a Lie subalgebra of $R$ and $L$. Let $x_{3}$ be a function from elements of $\SubtypeSet {x_{17}}{(\MembershipmemMACRoT {H}{x_{17}})}$ to elements of $R$. Let $x_{4}$ be a function from elements of $\SubtypeSet {x_{15}}{(\MembershipmemMACRoT {H}{x_{15}})}$ to elements of $R$. Let $x_{5}$ be a function from elements of $\SubtypeSet {x_{13}}{(\MembershipmemMACRoT {H}{x_{13}})}$ to elements of $R$ such that $\EqtMACRoH {x_{3} + x_{4}}{x_{5}}$. Then the root space product of $x_{4}$ and $x_{5}$ is a Lie module homomorphism of the set of tensor products of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{rootSpace} (H , x_{3})}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{rootSpace} (H , x_{4})}{x_{8}})}$ and $\SubtypeSet {x_{9}}{(\MembershipmemMACRoT {\operatorname{rootSpace} (H , x_{5})}{x_{9}})}$ defined as $\operatorname{rootSpaceWeightSpaceProduct}$ applied to $R$, $L$, $H$, $L$, $x_{3}$, $x_{4}$, $x_{5}$ and $h_{1}$.

LieAlgebra.rootSpaceWeightSpaceProductdefMathlib.Algebra.Lie.Weights.Cartan, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Let $H$ be a Lie subalgebra of $R$ and $L$. Let $x_{6}$ be a function from elements of $\SubtypeSet {x_{20}}{(\MembershipmemMACRoT {H}{x_{20}})}$ to elements of $R$. Let $x_{7}$ be a function from elements of $\SubtypeSet {x_{18}}{(\MembershipmemMACRoT {H}{x_{18}})}$ to elements of $R$. Let $x_{8}$ be a function from elements of $\SubtypeSet {x_{16}}{(\MembershipmemMACRoT {H}{x_{16}})}$ to elements of $R$ such that $\EqtMACRoH {x_{6} + x_{7}}{x_{8}}$. Then $\operatorname{rootSpaceWeightSpaceProduct}$ applied to $R$, $L$, $H$, $M$, $x_{6}$, $x_{7}$, $x_{8}$ and $h_{2}$ is a Lie module homomorphism of the set of tensor products of $\SubtypeSet {x_{10}}{(\MembershipmemMACRoT {\operatorname{rootSpace} (H , x_{6})}{x_{10}})}$ and $\SubtypeSet {x_{11}}{(\MembershipmemMACRoT {\operatorname{genWeightSpace} (M , x_{7})}{x_{11}})}$ and $\SubtypeSet {x_{12}}{(\MembershipmemMACRoT {\operatorname{genWeightSpace} (M , x_{8})}{x_{12}})}$.

LieAlgebra.zeroRootSubalgebradefMathlib.Algebra.Lie.Weights.Cartan, function or constant

Wording

the zero root subalgebra of H (from the name)

English

Let $R$ and $L$ be sets. Let $H$ be a Lie subalgebra of $R$ and $L$. Then the zero root subalgebra of $H$ is a Lie subalgebra of $R$ and $L$.

Mathlib.Algebra.Lie.Weights.Chain

LieModule.chainBotdefMathlib.Algebra.Lie.Weights.Chain, function or constant

Wording

the chain bottom of x6 and x7 (from the name)

English

Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Let $x_{7}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then the chain bottom of $x_{6}$ and $x_{7}$ is an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$.

LieModule.chainBotCoeffdefMathlib.Algebra.Lie.Weights.Chain, function or constant

Wording

the chain bottom coefficient of x6 and x7 (from the name)

English

Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Let $x_{7}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then the chain bottom coefficient of $x_{6}$ and $x_{7}$ is a natural number defined as the chain top coefficient of $\operatorname{neg}$ applied to $x_{6}$ and $x_{7}$.

LieModule.chainTopdefMathlib.Algebra.Lie.Weights.Chain, function or constant

Wording

the chain top of x6 and x7 (from the name)

English

Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Let $x_{7}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then the chain top of $x_{6}$ and $x_{7}$ is an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$.

LieModule.chainTopCoeffdefMathlib.Algebra.Lie.Weights.Chain, function or constant

Wording

the chain top coefficient of x6 and x7 (from the name)

English

Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Let $x_{7}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then the chain top coefficient of $x_{6}$ and $x_{7}$ is a natural number.

LieModule.genWeightSpaceChaindefMathlib.Algebra.Lie.Weights.Chain, function or constant

Wording

no wording

English

Let $M$ be a set. Let $x_{6}$ and $x_{7}$ be functions from elements of $L$ to elements of $R$. Let $p$ and $q$ be integers. Then $\operatorname{genWeightSpaceChain}$ applied to $M$, $x_{6}$, $x_{7}$, $p$ and $q$ is a Lie submodule of $L$ and $M$ defined as the supremum of the function that maps $k$ to the supremum of the function that maps $h_{2}$ to $\operatorname{genWeightSpace}$ applied to $M$ and $\HSMulhSMulMACRoAL {k}{x_{6}}+ x_{7}$.

Mathlib.Algebra.Lie.Weights.IsSimple

LieAlgebra.IsKilling.invtSubmoduleToLieIdealdefMathlib.Algebra.Lie.Weights.IsSimple, function or constant

Wording

no wording

English

Let $q$ be a submodule of $K$ and the set of duals of $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ such that for all elements $i$ of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{root}}{x_{3}})}$, $\MembershipmemMACRoT {\operatorname{invtSubmodule} (\operatorname{toLinearMap} (\operatorname{reflection} (\operatorname{rootSystem} (H), i)))}{q}$. Then $\operatorname{invtSubmoduleToLieIdeal}$ applied to $q$ and $\mathrm{hq}$ is a Lie ideal of $K$ and $L$.

LieAlgebra.IsKilling.lieIdealOrderIsodefMathlib.Algebra.Lie.Weights.IsSimple, function or constant

Wording

the Lie ideal order isomorphism of H (from the name)

English

Let $H$ be a Lie subalgebra of $K$ and $L$. Then the Lie ideal order isomorphism of $H$ is an order isomorphism of the set of Lie ideals of $K$ and $L$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{invtRootSubmodule} (\operatorname{rootSystem} (H))}{x_{3}})}$.

LieIdeal.rootSetdefMathlib.Algebra.Lie.Weights.IsSimple, function or constant

Wording

the root set of I (from the name)

English

Let $I$ be a Lie ideal of $K$ and $L$. Then the root set of $I$ is an element of $\wp (\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{root}}{x_{3}})})$ defined as $\operatorname{ofPred}$ applied to the function that maps $x_{3}$ to $\mathrm{Leq} (\operatorname{rootSpace} (H , \operatorname{coe} (x_{3})), \operatorname{restr} (I , H))$.

LieIdeal.rootSpandefMathlib.Algebra.Lie.Weights.IsSimple, function or constant

Wording

the root span of I (from the name)

English

Let $I$ be a Lie ideal of $K$ and $L$. Then the root span of $I$ is a submodule of $K$ and the set of duals of $K$ and $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ defined as the span of $K$ and the image of $\operatorname{coe}$ applied to the root of the root system of $H$ and the root set of $I$.

LieIdeal.toInvtRootSubmoduledefMathlib.Algebra.Lie.Weights.IsSimple, function or constant

Wording

the invariant root submodule corresponding to a Lie ideal of I (from the docstring)

English

Let $I$ be a Lie ideal of $K$ and $L$. Then the invariant root submodule corresponding to a Lie ideal of $I$ is an element of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {\operatorname{invtRootSubmodule} (\operatorname{rootSystem} (H))}{x_{3}})}$ defined as the root span of $I$.

Mathlib.Algebra.Lie.Weights.Killing

LieAlgebra.IsKilling.cartanEquivDualdefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

the Cartan equivalence dual of H (from the name)

English

Let $H$ be a Lie subalgebra of $K$ and $L$. Then the Cartan equivalence dual of $H$ is a linear equivalence of $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and the set of duals of $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$.

LieAlgebra.IsKilling.corootdefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

the coroot corresponding to a root of x3 (from the docstring)

English

Let $x_{3}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $L$. Then the coroot corresponding to a root of $x_{3}$ is an element of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ defined as $\HSMulhSMulMACRoAL {2}{(\HSMulhSMulMACRoAL {\operatorname{inv} (x_{3} (\operatorname{symm} (\operatorname{cartanEquivDual} (H), \operatorname{toLinear} (K , \SubtypeSet {x_{8}}{(\MembershipmemMACRoT {H}{x_{8}})}, L , x_{3}))))}{\operatorname{symm} (\operatorname{cartanEquivDual} (H), \operatorname{toLinear} (K , \SubtypeSet {x_{9}}{(\MembershipmemMACRoT {H}{x_{9}})}, L , x_{3}))})}$.

LieAlgebra.IsKilling.corootSubmoduledefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

the coroot space of x3 (from the docstring)

English

Let $x_{3}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $L$. Then the coroot space of $x_{3}$ is a Lie submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $L$ defined as the map of the inclusion of the Lie submodule of $H$ and the coroot space of $\operatorname{coe}$ applied to $x_{3}$.

LieAlgebra.IsKilling.sl2SubalgebraOfRootdefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

no wording

English

Assume that $x_{3}$ is non zero. Then $\operatorname{sl2SubalgebraOfRoot}$ applied to $h_{5}$ is a Lie subalgebra of $K$ and $L$.

LieAlgebra.IsKilling.sl2SubmoduleOfRootdefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

no wording

English

Assume that $x_{3}$ is non zero. Then $\operatorname{sl2SubmoduleOfRoot}$ applied to $h_{5}$ is a Lie submodule of $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $L$.

LieSubalgebra.rootdefMathlib.Algebra.Lie.Weights.Killing, function or constant

Wording

the root (from the name)

English

The root is a finite set of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{3}}{(\MembershipmemMACRoT {H}{x_{3}})}$ and $L$ defined as $\FinsetFilter {x_{3}}{\operatorname{IsNonZero} (x_{3})}{\FinsetunivMACRoAC}$.

Mathlib.Algebra.Lie.Weights.Linear

LieModule.LinearWeightsclassMathlib.Algebra.Lie.Weights.Linear, predicate

Wording

no wording

English

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

LieModule.Weight.kerdefMathlib.Algebra.Lie.Weights.Linear, function or constant

Wording

the kernel (from the docstring)

English

The kernel is a submodule of $R$ and $L$ defined as the kernel of $\operatorname{toLinear}$ applied to $R$, $L$, $M$ and $x_{6}$.

LieModule.Weight.toLineardefMathlib.Algebra.Lie.Weights.Linear, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Let $x_{6}$ be an element of $\operatorname{Weight}$ applied to $R$, $L$ and $M$. Then $\operatorname{toLinear}$ applied to $R$, $L$, $M$ and $x_{6}$ is a linear map of $L$ and $R$.

LieModule.shiftedGenWeightSpacedefMathlib.Algebra.Lie.Weights.Linear, function or constant

Wording

no wording

English

Let $R$, $L$ and $M$ be sets. Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Then $\operatorname{shiftedGenWeightSpace}$ applied to $R$, $L$, $M$ and $x_{6}$ is a Lie submodule of $L$ and $M$ defined as $\operatorname{genWeightSpace}$ applied to $M$ and $x_{6}$.

LieModule.shiftedGenWeightSpace.shiftdefMathlib.Algebra.Lie.Weights.Linear, function or constant

Wording

the shift of x6 (from the name)

English

Let $R$, $L$ and $M$ be sets. Let $x_{6}$ be a function from elements of $L$ to elements of $R$. Then the shift of $x_{6}$ is a linear equivalence of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{genWeightSpace} (M , x_{6})}{x_{7}})}$ and $\SubtypeSet {x_{8}}{(\MembershipmemMACRoT {\operatorname{shiftedGenWeightSpace} (R , L , M , x_{6})}{x_{8}})}$ defined as the identity map of $R$ and $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\operatorname{genWeightSpace} (M , x_{6})}{x_{7}})}$.

Mathlib.Algebra.Lie.Weights.RootSystem

LieAlgebra.IsKilling.chainLengthdefMathlib.Algebra.Lie.Weights.RootSystem, function or constant

Wording

the chain length of x3 and x4 (from the name)

English

Let $x_{3}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {H}{x_{6}})}$ and $L$. Let $x_{4}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $L$. Then the chain length of $x_{3}$ and $x_{4}$ is a natural number.

LieAlgebra.IsKilling.reflectRootdefMathlib.Algebra.Lie.Weights.RootSystem, function or constant

Wording

the reflection of x3 and x4 (from the docstring)

English

Let $x_{3}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {H}{x_{7}})}$ and $L$. Let $x_{4}$ be an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{6}}{(\MembershipmemMACRoT {H}{x_{6}})}$ and $L$. Then the reflection of $x_{3}$ and $x_{4}$ is an element of $\operatorname{Weight}$ applied to $K$, $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$ and $L$.

LieAlgebra.IsKilling.rootSystemdefMathlib.Algebra.Lie.Weights.RootSystem, function or constant

Wording

the root system of H (from the docstring)

English

Let $H$ be a Lie subalgebra of $K$ and $L$. Then the root system of $H$ is a root pairing of the set of duals of $K$ and $\SubtypeSet {x_{4}}{(\MembershipmemMACRoT {H}{x_{4}})}$ and $\SubtypeSet {x_{5}}{(\MembershipmemMACRoT {H}{x_{5}})}$.

Mathlib.Algebra.LieRinehartAlgebra.Defs

LieRinehartAlgebraclassMathlib.Algebra.LieRinehartAlgebra.Defs, predicate

Wording

no wording

English

Let $R$, $A$ and $L$ be sets. Then we can say that $\mathrm{LieRinehartAlgebra}$ holds for $R$, $A$ and $L$.

LieRinehartAlgebra.HomstructureMathlib.Algebra.LieRinehartAlgebra.Defs, type

Wording

homomorphism of x8 and x9 (from the name)

English

Let $x_{7}$ be an algebra homomorphism of $x$ and $x_{1}$. Let $x_{8}$ and $x_{9}$ be sets. Then the homomorphisms of $x_{8}$ and $x_{9}$ are a basic type.

LieRinehartAlgebra.Hom.compdefMathlib.Algebra.LieRinehartAlgebra.Defs, function or constant

Wording

the composition of f and g (from the name)

English

Let $f$ be a homomorphism of $x_{1}$ and $x_{3}$. Let $g$ be a homomorphism of $x_{3}$ and $x_{5}$. Then the composition of $f$ and $g$ is a homomorphism of $x_{1}$ and $x_{5}$.

LieRinehartAlgebra.Hom.iddefMathlib.Algebra.LieRinehartAlgebra.Defs, function or constant

Wording

the identity morphism (from the docstring)

English

The identity morphism is a homomorphism of $x_{1}$ and $x_{1}$.

LieRinehartAlgebra.Hom.toLinearMap'defMathlib.Algebra.LieRinehartAlgebra.Defs, function or constant

Wording

the linear map of f (from the name)

English

Let $f$ be a homomorphism of $x_{1}$ and $x_{3}$. Then the linear map of $f$ is a linear map of $x_{1}$ and $x_{3}$.

LieRinehartAlgebra.anchordefMathlib.Algebra.LieRinehartAlgebra.Defs, function or constant

Wording

no wording

English

Let $R$, $x$ and $x_{1}$ be sets. Then $\operatorname{anchor}$ applied to $R$, $x$ and $x_{1}$ is a homomorphism of $x_{1}$ and the set of derivations of $x$ and $x$.

LieRinehartRingclassMathlib.Algebra.LieRinehartAlgebra.Defs, predicate

Wording

no wording

English

Let $A$ and $L$ be sets. Then we can say that $\mathrm{LieRinehartRing}$ holds for $A$ and $L$.

Mathlib.Algebra.LieRinehartAlgebra.Subalgebra

LieRinehartSubalgebrastructureMathlib.Algebra.LieRinehartAlgebra.Subalgebra, type

Wording

no wording

English

Let $A$ and $L$ be sets. Then the elements of $\mathrm{LieRinehartSubalgebra}$ applied to $A$ and $L$ are a basic type.

LieRinehartSubalgebra.incldefMathlib.Algebra.LieRinehartAlgebra.Subalgebra, function or constant

Wording

the inclusion of R and #2 (from the name)

English

Let $\mathrm{L'}$ be an element of $\mathrm{LieRinehartSubalgebra}$ applied to $A$ and $L$. Let $R$ be a set. Then the inclusion of $\mathrm{L'}$ and $R$ is a homomorphism of $\SubtypeSet {x_{7}}{(\MembershipmemMACRoT {\mathrm{L'}}{x_{7}})}$ and $L$.

LieRinehartSubalgebra.toLieSubalgebradefMathlib.Algebra.LieRinehartAlgebra.Subalgebra, function or constant

Wording

the Lie subalgebra of R and #2 (from the name)

English

Let $\mathrm{L'}$ be an element of $\mathrm{LieRinehartSubalgebra}$ applied to $A$ and $L$. Let $R$ be a set. Then the Lie subalgebra of $\mathrm{L'}$ and $R$ is a Lie subalgebra of $R$ and $L$ defined as $\operatorname{mk}$ applied to $\operatorname{restrictScalars}$ applied to $R$ and $\operatorname{toSubmodule}$ applied to $\mathrm{L'}$ and the function that maps $x_{7}$ and $x_{8}$ to $\mathrm{LieRinehartSubalgebra\_\_lie\_mem'}$ applied to $\mathrm{L'}$.

Mathlib.Algebra.LinearRecurrence

LinearRecurrencestructureMathlib.Algebra.LinearRecurrence, type

Wording

linear recurrence of R (from the name)

English

Let $R$ be a set. Then the linear recurrences of $R$ are a basic type.

LinearRecurrence.IsSolutiondefMathlib.Algebra.LinearRecurrence, predicate

Wording

no wording

English

Let $E$ be a linear recurrence of $R$. Let $u$ be a function from natural numbers to elements of $R$. Then $\operatorname{IsSolution}$ holds for $E$ and $u$, if for all natural numbers $n$, $u$ applied to the sum of $n$ and the order of $E$ is equal to $\FinsetSum {\FinsetunivMACRoAC}{i}{(\operatorname{coeffs} (E , i)\times u (n + \operatorname{val} (i)))}$.

LinearRecurrence.basisdefMathlib.Algebra.LinearRecurrence, function or constant

Wording

the basis of E (from the name)

English

Let $E$ be a linear recurrence of $R$. Then the basis of $E$ is a basis of $R$ and $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{solSpace} (E)}{x_{1}})}$ defined as the basis of $\operatorname{toInit}$ applied to $E$.

LinearRecurrence.charPolydefMathlib.Algebra.LinearRecurrence, function or constant

Wording

the characteristic polynomial of E (from the docstring)

English

Let $E$ be a linear recurrence of $R$. Then the characteristic polynomial of $E$ is a polynomial of $R$ defined as the difference between $\operatorname{monomial}$ applied to the order of $E$ and $1$ and $\FinsetSum {\FinsetunivMACRoAC}{i}{\operatorname{monomial} (\operatorname{val} (i), \operatorname{coeffs} (E , i))}$.

LinearRecurrence.coeffsdefMathlib.Algebra.LinearRecurrence, function or constant

Wording

no wording

English

Let $\mathrm{self}$ be a linear recurrence of $R$. Let $x_{1}$ be an element of $\mathrm{Fin}$ applied to the order of $\mathrm{self}$. Then $\operatorname{coeffs}$ applied to $\mathrm{self}$ and $x_{1}$ is an element of $R$ defined as $\operatorname{proj1}$ applied to $\mathrm{self}$ and $x_{1}$.

LinearRecurrence.mkSoldefMathlib.Algebra.LinearRecurrence, function or constant

Wording

no wording

English

Let $E$ be a linear recurrence of $R$. Let $\mathrm{init}$ be a function from elements of $\mathrm{Fin}$ applied to the order of $E$ to elements of $R$. Let $x_{1}$ be a natural number. Then $\operatorname{mkSol}$ applied to $E$, $\mathrm{init}$ and $x_{1}$ is an element of $R$.

LinearRecurrence.orderdefMathlib.Algebra.LinearRecurrence, function or constant

Wording

the order of self (from the name)

English

Let $\mathrm{self}$ be a linear recurrence of $R$. Then the order of $\mathrm{self}$ is a natural number defined as $\operatorname{proj0}$ applied to $\mathrm{self}$.

LinearRecurrence.solSpacedefMathlib.Algebra.LinearRecurrence, function or constant

Wording

no wording

English

Let $E$ be a linear recurrence of $R$. Then $\operatorname{solSpace}$ applied to $E$ is a submodule of $R$ and the set of functions from natural numbers to elements of $R$.

LinearRecurrence.toInitdefMathlib.Algebra.LinearRecurrence, function or constant

Wording

no wording

English

Let $E$ be a linear recurrence of $R$. Then $\operatorname{toInit}$ applied to $E$ is a linear equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{solSpace} (E)}{x_{1}})}$ and the set of functions from elements of $\mathrm{Fin}$ applied to the order of $E$ to elements of $R$.

LinearRecurrence.tupleSuccdefMathlib.Algebra.LinearRecurrence, function or constant

Wording

the tuple successor of E (from the name)

English

Let $E$ be a linear recurrence of $R$. Then the tuple successor of $E$ is a linear map of the set of functions from elements of $\mathrm{Fin}$ applied to the order of $E$ to elements of $R$ and the set of functions from elements of $\mathrm{Fin}$ applied to the order of $E$ to elements of $R$.

Mathlib.Algebra.Module.Bimodule

Subbimodule.baseChangedefMathlib.Algebra.Module.Bimodule, function or constant

Wording

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

English

Let $S$ be a set. Let $p$ be a submodule of the set of tensor products of $A$ and $B$ and $M$. Then the base change of $S$ and $p$ is a submodule of the set of tensor products of $A$ and $B$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{toAddSubmonoid}$ applied to $p$, $\mathrm{Subbimodule\_\_smul\_mem}$ applied to $p$ and $\mathrm{Subbimodule\_\_smul\_mem'}$ applied to $p$.

Subbimodule.mkdefMathlib.Algebra.Module.Bimodule, function or constant

Wording

no wording

English

Let $p$ be an additive submonoid of $M$ such that for all elements $a$ of $A$, for all elements $m_{1}$ of $M$, if $m_{1}$ is an element of $p$, then $\HSMulhSMulMACRoAL {a}{m_{1}}$ is an element of $p$ and for all elements $b$ of $B$, for all elements $m$ of $M$, if $m$ is an element of $p$, then $\HSMulhSMulMACRoAL {b}{m}$ is an element of $p$. Then $\operatorname{mk}$ applied to $p$, $\mathrm{hA}$ and $\mathrm{hB}$ is a submodule of the set of tensor products of $A$ and $B$ and $M$.

Subbimodule.toSubbimoduleIntdefMathlib.Algebra.Module.Bimodule, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Let $p$ be a submodule of the set of tensor products of $R$ and $S$ and $M$. Then $\operatorname{toSubbimoduleInt}$ applied to $R$, $S$, $M$ and $p$ is a submodule of the set of tensor products of $R$ and $S$ and $M$ defined as the base change of $\Integer$ and $p$.

Subbimodule.toSubbimoduleNatdefMathlib.Algebra.Module.Bimodule, function or constant

Wording

no wording

English

Let $R$, $S$ and $M$ be sets. Let $p$ be a submodule of the set of tensor products of $R$ and $S$ and $M$. Then $\operatorname{toSubbimoduleNat}$ applied to $R$, $S$, $M$ and $p$ is a submodule of the set of tensor products of $R$ and $S$ and $M$ defined as the base change of $\Natural$ and $p$.

Subbimodule.toSubmoduledefMathlib.Algebra.Module.Bimodule, function or constant

Wording

the submodule of p (from the name)

English

Let $p$ be a submodule of the set of tensor products of $A$ and $B$ and $M$. Then the submodule of $p$ is a submodule of $A$ and $M$.

Subbimodule.toSubmodule'defMathlib.Algebra.Module.Bimodule, function or constant

Wording

the submodule of p (from the name)

English

Let $p$ be a submodule of the set of tensor products of $A$ and $B$ and $M$. Then the submodule of $p$ is a submodule of $B$ and $M$.

Mathlib.Algebra.Module.CharacterModule

CharacterModuledefMathlib.Algebra.Module.CharacterModule, type

Wording

character module of A (from the name)

English

Let $A$ be a set. Then a character module of $A$ is an element of the function that maps $A$ to the set of additive monoid homomorphisms of $A$ and the set of additive circles of $1$.

CharacterModule.congrdefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the congruence of e (from the name)

English

Let $e$ be a linear equivalence of $A$ and $B$. Then the congruence of $e$ is a linear equivalence of the set of character modules of $A$ and the set of character modules of $B$.

CharacterModule.currydefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the curry (from the name)

English

The curry is a linear map of the set of character modules of the set of tensor products of $A$ and $B$ and the set of linear maps of $A$ and the set of character modules of $B$.

CharacterModule.dualdefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the dual of f (from the name)

English

Let $f$ be a linear map of $A$ and $B$. Then the dual of $f$ is a linear map of the set of character modules of $B$ and the set of character modules of $A$.

CharacterModule.homEquivdefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the homomorphism equivalence (from the name)

English

The homomorphism equivalence is a linear equivalence of the set of linear maps of $A$ and the set of character modules of $B$ and the set of character modules of the set of tensor products of $A$ and $B$.

CharacterModule.intdefMathlib.Algebra.Module.CharacterModule, type

Wording

integer (from the name)

English

An integer is a character module of $\Integer$.

CharacterModule.int.divByNatdefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the quotient by natural number of n (from the name)

English

Let $n$ be a natural number. Then the quotient by natural number of $n$ is an integer defined as the additive monoid homomorphism of the span singleton of $\operatorname{mk}$ applied to $\operatorname{inv}$ applied to $n$.

CharacterModule.intSpanEquivQuotAddOrderOfdefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the integer span equivalence quotient additive order of a (from the name)

English

Let $a$ be an element of $A$. Then the integer span equivalence quotient additive order of $a$ is a linear equivalence of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{span} (\Integer , \operatorname{singleton} (a))}{x_{1}})}$ and the set of quotients of $\Integer$ and the span of $\operatorname{singleton}$ applied to the additive order of $a$.

CharacterModule.ofSpanSingletondefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

the character module of a (from the name)

English

Let $a$ be an element of $A$. Then the character module of $a$ is a character module of $\SubtypeSet {x_{1}}{(\MembershipmemMACRoT {\operatorname{span} (\Integer , \operatorname{singleton} (a))}{x_{1}})}$.

CharacterModule.uncurrydefMathlib.Algebra.Module.CharacterModule, function or constant

Wording

no wording

English

$\operatorname{uncurry}$ is a linear map of the set of linear maps of $A$ and the set of character modules of $B$ and the set of character modules of the set of tensor products of $A$ and $B$.

Mathlib.Algebra.Module.Congruence.Defs

ModuleConstructureMathlib.Algebra.Module.Congruence.Defs, type

Wording

module congruence relation of S and M (from the name)

English

Let $S$ and $M$ be sets. Then the module congruence relations of $S$ and $M$ are a basic type.

ModuleCon.QuotientdefMathlib.Algebra.Module.Congruence.Defs, type

Wording

quotient of M and c (from the name)

English

Let $M$ be a set. Let $c$ be a module congruence relation of $S$ and $M$. Then a quotient of $M$ and $c$ is an element of the function that maps $M$ and $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $\operatorname{toAddCon}$ applied to $c$.

ModuleCon.kerdefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a distributive multiplicative action homomorphism of $M$ and $N$. Then the kernel of $f$ is a module congruence relation of $R$ and $M$.

ModuleCon.quotientKerEquivOfSurjectivedefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

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

English

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

ModuleCon.toSMulCondefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the multiplicative congruence relation of self (from the name)

English

Let $\mathrm{self}$ be a module congruence relation of $S$ and $M$. Then the multiplicative congruence relation of $\mathrm{self}$ is a multiplicative congruence relation of $S$ and $M$ defined as $\operatorname{mk}$ applied to $\operatorname{toSetoid}$ applied to $\operatorname{toAddCon}$ applied to $\mathrm{self}$ and $\operatorname{smul}$ applied to $\mathrm{self}$.

SMulConstructureMathlib.Algebra.Module.Congruence.Defs, type

Wording

multiplicative congruence relation of S and M (from the name)

English

Let $S$ and $M$ be sets. Then the multiplicative congruence relations of $S$ and $M$ are a basic type.

SMulCon.QuotientdefMathlib.Algebra.Module.Congruence.Defs, type

Wording

quotient of M and c (from the name)

English

Let $M$ be a set. Let $c$ be a multiplicative congruence relation of $S$ and $M$. Then a quotient of $M$ and $c$ is an element of the function that maps $M$ and $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $c$.

SMulCon.addConGendefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the additive congruence relation generator of c (from the name)

English

Let $c$ be a multiplicative congruence relation of $S$ and $M$. Then the additive congruence relation generator of $c$ is a module congruence relation of $S$ and $M$.

SMulCon.addConGen'defMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the additive congruence relation generator of r and hr (from the name)

English

Let $r$ be a function from elements of $M$ and elements of $M$ to propositions such that for all elements $s$ of $S$, for all elements $m$ and $\mathrm{m'}$ of $M$, if $r$ holds for $m$ and $\mathrm{m'}$, then $r$ holds for $\HSMulhSMulMACRoAL {s}{m}$ and $\HSMulhSMulMACRoAL {s}{\mathrm{m'}}$. Then the additive congruence relation generator of $r$ and $\mathrm{hr}$ is a module congruence relation of $S$ and $M$.

SMulCon.kerdefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be a multiplicative action homomorphism of $M$ and $N$. Then the kernel of $f$ is a multiplicative congruence relation of $R$ and $M$.

VAddConstructureMathlib.Algebra.Module.Congruence.Defs, type

Wording

additive congruence relation of S and M (from the name)

English

Let $S$ and $M$ be sets. Then the additive congruence relations of $S$ and $M$ are a basic type.

VAddCon.QuotientdefMathlib.Algebra.Module.Congruence.Defs, type

Wording

quotient of M and c (from the name)

English

Let $M$ be a set. Let $c$ be an additive congruence relation of $S$ and $M$. Then a quotient of $M$ and $c$ is an element of the function that maps $M$ and $c$ to $\mathrm{Quotient}$ applied to $\operatorname{toSetoid}$ applied to $c$.

VAddCon.kerdefMathlib.Algebra.Module.Congruence.Defs, function or constant

Wording

the kernel of f (from the docstring)

English

Let $f$ be an additive action homomorphism of $M$ and $N$. Then the kernel of $f$ is an additive congruence relation of $R$ and $M$.

Mathlib.Algebra.Module.Defs

ModuleclassMathlib.Algebra.Module.Defs, predicate

Wording

no wording

English

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

Mathlib.Algebra.Module.End

Module.toAddMonoidEnddefMathlib.Algebra.Module.End, function or constant

Wording

the additive monoid end of R and M (from the name)

English

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

smulAddHomdefMathlib.Algebra.Module.End, function or constant

Wording

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

English

Let $R$ and $M$ be sets. Then the scalar multiple additive homomorphism of $R$ and $M$ 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$.