WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Root system

Revision #1547 → #1796 · back to history

modifiedCosine of angle between roots is constrained5afaa5c3db1d
FieldFrom #1547To #1796
anchors[{"section":"Elementary consequences of the root system axioms","snippet":"The cosine of the angle between two roots is constrained to be one-half of the square root of a positive integer"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\langle \\beta ,\\alpha \\rangle \\langle \\alpha ,\\beta \\rangle &=2{\\frac {(\\alpha ,\\beta )}{(\\alpha ,\\alpha )}}\\cdot 2{\\frac {(\\alpha ,\\beta )}{(\\beta ,\\beta )}}\\\\&=4{\\frac {(\\alpha ,\\beta )^{2}}{\\vert \\alpha \\vert ^{2}\\vert \\beta \\vert ^{2}}}\\\\&=4\\cos ^{2}(\\theta )\\\\&=(2\\cos(\\theta ))^{2}\\in \\mathbb {Z} .\\end{aligned}}}"}][{"section":"Elementary consequences of the root system axioms","snippet":"The cosine of the angle between two roots is constrained to be one-half of the square root of a positive integer"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\langle \\beta ,\\alpha \\rangle \\langle \\alpha ,\\beta \\rangle &=2{\\frac {(\\alpha ,\\beta )}{(\\alpha ,\\alpha )}}\\cdot 2{\\frac {(\\alpha ,\\beta )}{(\\beta ,\\beta )}}\\\\&=4{\\frac {(\\alpha ,\\beta )^{2}}{\\vert \\alpha \\vert ^{2}\\vert \\beta \\vert ^{2}}}\\\\&=4\\cos ^{2}(\\theta )\\\\&=(2\\cos(\\theta ))^{2}\\in \\mathbb {Z} .\\end{aligned}}}"}]
modifiedFour classical families and five exceptional cases0ffa4bd6903d
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedSimply laced root system97fec42b7b2d
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe Aₙ root system6a947bf5c471
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe Bₙ root systemf78f118ebcee
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedB1 is isomorphic to A1cd14f8cfb802
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe Cₙ root system0ab179dd01f1
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedC2 is isomorphic to B2b02c31cbc680
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe Dₙ root system89bd1ce4f880
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedD3 coincides with A347e619e48dfa
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe E8 root system5327b7291de2
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe E7 root system37dd0eb81885
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe E6 root systemdb71e77901f6
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan
modifiedThe F4 root system48a18ea936fd
FieldFrom #1547To #1796
mathlib.moduleMathlib.Data.Matrix.CartanMathlib.LinearAlgebra.Matrix.Cartan