Documentation

Project.IntegralLattice.E8.Basic

class E8Lattice (Λ : Type u_1) extends IntegralLattice Λ :
Type u_1

The E8 lattice is the unique even, unimodular integral lattice of rank 8

Instances
    theorem E8Lattice.unique (Λ₁ : Type u_2) (Λ₂ : Type u_3) [E8Lattice Λ₁] [E8Lattice Λ₂] :
    Nonempty (Λ₁ ≃ₗ Λ₂)
    def E8Lattice.intMatrixToRat {m n : } (A : Matrix (Fin m) (Fin n) ) :
    Matrix (Fin m) (Fin n)
    Equations
    Instances For
      theorem E8Lattice.intDetToRat {n : } (A : Matrix (Fin n) (Fin n) ) :
      theorem E8Lattice.inner_self_calc (x : Fin 8) :
      (B x) x = 2 * (x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 + x 4 ^ 2 + x 5 ^ 2 + x 6 ^ 2 + x 7 ^ 2 - (x 0 * x 2 + x 1 * x 3 + x 2 * x 3 + x 3 * x 4 + x 4 * x 5 + x 5 * x 6 + x 6 * x 7))
      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
      theorem E8Lattice.AddInner (x y z : Fin 8) :
      (B (x + y)) z = (B x) z + (B y) z
      theorem E8Lattice.InnerSym (x y : Fin 8) :
      (B x) y = (B y) x
      theorem E8Lattice.InnerSelf (x : Fin 8) :
      (B x) x 0
      theorem E8Lattice.InnerEven (x : Fin 8) :
      Even ((B x) x)
      theorem E8Lattice.InnerSelfEqZero (x : Fin 8) :
      (B x) x = 0x = 0
      Equations
      • One or more equations did not get rendered due to their size.
      theorem E8Lattice.exists_E8 :
      ∃ (Λ : Type u), Nonempty (E8Lattice Λ)
      instance E8Lattice.instFiniteElemSetOfEqIntInnerCast (Λ : Type u_1) [E8Lattice Λ] (n : ) :
      Finite {x : Λ | inner x x = n}
      instance E8Lattice.instFiniteSubtypeEqIntInnerCast (Λ : Type u_1) [E8Lattice Λ] (n : ) :
      Finite { x : Λ // inner x x = n }
      theorem E8Lattice.card_norm_2 (Λ : Type u_1) [E8Lattice Λ] :
      Nat.card {x : Λ | inner x x = 2} = 240