The E8 lattice is the unique even, unimodular integral lattice of rank 8
- add : Λ → Λ → Λ
- zero : Λ
- neg : Λ → Λ
- sub : Λ → Λ → Λ
- free : Module.Free ℤ Λ
- finite : Module.Finite ℤ Λ
- even : IntegralLattice.IsEven Λ
- unimodular : IntegralLattice.IsUnimodular Λ
Instances
Equations
Instances For
Instances For
Equations
- E8Lattice.M1 = E8Lattice.M0.updateRow 2 (E8Lattice.M0 2 + (1 / 2) • E8Lattice.M0 0)
Instances For
Equations
- E8Lattice.M2 = E8Lattice.M1.updateRow 3 (E8Lattice.M1 3 + (1 / 2) • E8Lattice.M1 1)
Instances For
Equations
- E8Lattice.M3 = E8Lattice.M2.updateRow 3 (E8Lattice.M2 3 + (2 / 3) • E8Lattice.M2 2)
Instances For
Equations
- E8Lattice.M4 = E8Lattice.M3.updateRow 4 (E8Lattice.M3 4 + (6 / 5) • E8Lattice.M3 3)
Instances For
Equations
- E8Lattice.M5 = E8Lattice.M4.updateRow 5 (E8Lattice.M4 5 + (5 / 4) • E8Lattice.M4 4)
Instances For
Equations
- E8Lattice.M6 = E8Lattice.M5.updateRow 6 (E8Lattice.M5 6 + (4 / 3) • E8Lattice.M5 5)
Instances For
Equations
- E8Lattice.M7 = E8Lattice.M6.updateRow 7 (E8Lattice.M6 7 + (3 / 2) • E8Lattice.M6 6)
Instances For
theorem
E8Lattice.inner_self_comp_sq
(x : Fin 8 → ℤ)
:
↑((B x) x) = (√2 * ↑(x 0) - √(1 / 2) * ↑(x 2)) ^ 2 + (√2 * ↑(x 1) - √(1 / 2) * ↑(x 3)) ^ 2 + (√(3 / 2) * ↑(x 2) - √(2 / 3) * ↑(x 3)) ^ 2 + (√(5 / 6) * ↑(x 3) - √(6 / 5) * ↑(x 4)) ^ 2 + (√(4 / 5) * ↑(x 4) - √(5 / 4) * ↑(x 5)) ^ 2 + (√(3 / 4) * ↑(x 5) - √(4 / 3) * ↑(x 6)) ^ 2 + (√(2 / 3) * ↑(x 6) - √(3 / 2) * ↑(x 7)) ^ 2 + 1 / 2 * ↑(x 7) ^ 2
Equations
- One or more equations did not get rendered due to their size.