The E₈-lattice

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-07-28.
Last modified on 2023-06-08.

module group-theory.e8-lattice where
Imports 
open import elementary-number-theory.integers

open import foundation.equality-coproduct-types
open import foundation.sets
open import foundation.universe-levels

open import univalent-combinatorics.standard-finite-types

Definition

The ambient set of the E₈ lattice

The E₈ lattice itself is a subset of the following set.

ambient-set-E8-lattice : Set lzero
ambient-set-E8-lattice =
  coprod-Set (hom-Set (Fin-Set 8) ℤ-Set) (hom-Set (Fin-Set 8) ℤ-Set)

Recent changes