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
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).