SerreConstruction
📁 Source: Mathlib/Algebra/Lie/SerreConstruction.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsEF, HE, HF, HH, adE, adF, toIdeal, toSet, aₙ, bₙ, cₙ, dₙ, instInhabitedGenerators, e₆, e₇, e₈, f₄, g₂, ToLieAlgebra, instInhabitedToLieAlgebra, instLieAlgebraToLieAlgebra, instLieRingToLieAlgebra | 22 |
| Theorems | 0 |
| Total | 22 |
CartanMatrix
Definitions
| Name | Category | Theorems |
|---|---|---|
aₙ 📖 | CompOp | — |
bₙ 📖 | CompOp | — |
cₙ 📖 | CompOp | — |
dₙ 📖 | CompOp | — |
instInhabitedGenerators 📖 | CompOp | — |
CartanMatrix.Relations
Definitions
| Name | Category | Theorems |
|---|---|---|
EF 📖 | CompOp | — |
HE 📖 | CompOp | — |
HF 📖 | CompOp | — |
HH 📖 | CompOp | — |
adE 📖 | CompOp | — |
adF 📖 | CompOp | — |
toIdeal 📖 | CompOp | — |
toSet 📖 | CompOp | — |
LieAlgebra
Definitions
| Name | Category | Theorems |
|---|---|---|
e₆ 📖 | CompOp | — |
e₇ 📖 | CompOp | — |
e₈ 📖 | CompOp | — |
f₄ 📖 | CompOp | — |
g₂ 📖 | CompOp | — |
Matrix
Definitions
| Name | Category | Theorems |
|---|---|---|
ToLieAlgebra 📖 | CompOp | — |
instInhabitedToLieAlgebra 📖 | CompOp | — |
instLieAlgebraToLieAlgebra 📖 | CompOp | — |
instLieRingToLieAlgebra 📖 | CompOp | — |
---