The E₈-lattice

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

Created on 2022-07-28.
Last modified on 2024-02-06.

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 =
  coproduct-Set (hom-set-Set (Fin-Set 8) ℤ-Set) (hom-set-Set (Fin-Set 8) ℤ-Set)

Recent changes