theorem span_E8Matrix.{u_2} (RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  RType u_2] [CharZeroCharZero.{u_1} (R : Type u_1) [AddMonoidWithOne R] : PropTypeclass for monoids with characteristic zero.
  (This is usually stated on fields but it makes sense for any additive monoid with 1.)

*Warning*: for a semiring `R`, `CharZero R` and `CharP R 0` need not coincide.
* `CharZero R` requires an injection `ℕ ↪ R`;
* `CharP R 0` asks that only `0 : ℕ` maps to `0 : R` under the map `ℕ → R`.
  For instance, endowing `{0, 1}` with addition given by `max` (i.e. `1` is absorbing), shows that
  `CharZero {0, 1}` does not hold and yet `CharP {0, 1} 0` does.
  This example is formalized in `Counterexamples/CharPZeroNeCharZero.lean`.
 RType u_2] :
  Submodule.spanSubmodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.  ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).

      (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  (E8MatrixE8Matrix.{u_2} (R : Type u_2) [Field R] : Matrix (Fin 8) (Fin 8) R RType u_2).rowMatrix.row.{v, u_2, u_3} {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : m → n → αFor an `m × n` `α`-matrix `A`, `A.row i` is the `i`th row of `A` as a vector in `n → α`.
`A.row` is defeq to `A`, but explicitly refers to the 'row function' of `A`
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like `Set.Injective A.row` and `Set.range A.row`.
(Note 2025-04-07 : the identifier `Matrix.row` used to refer to a matrix with all rows equal;
this is now called `Matrix.replicateRow`) ) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    Submodule.E8Submodule.E8.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule ℤ (Fin 8 → R) RType u_2

theorem span_E8Matrix_eq_top.{u_2} (RType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements.

An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`.
Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need
to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself).
See also note [forgetful inheritance].

If the field has positive characteristic `p`, our division by zero convention forces
`ratCast (1 / p) = 1 / 0 = 0`.  RType u_2] [NeZeroNeZero.{u_1} {R : Type u_1} [Zero R] (n : R) : PropA type-class version of `n ≠ 0`.   2] :
  Submodule.spanSubmodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
  Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.  RType u_2
      (Set.rangeSet.range.{u, u_1} {α : Type u} {ι : Sort u_1} (f : ι → α) : Set αRange of a function.

This function is more flexible than `f '' univ`, as the image requires that the domain is in Type
and not an arbitrary Sort.  (E8MatrixE8Matrix.{u_2} (R : Type u_2) [Field R] : Matrix (Fin 8) (Fin 8) R RType u_2).rowMatrix.row.{v, u_2, u_3} {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) : m → n → αFor an `m × n` `α`-matrix `A`, `A.row i` is the `i`th row of `A` as a vector in `n → α`.
`A.row` is defeq to `A`, but explicitly refers to the 'row function' of `A`
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like `Set.Injective A.row` and `Set.range A.row`.
(Note 2025-04-07 : the identifier `Matrix.row` used to refer to a matrix with all rows equal;
this is now called `Matrix.replicateRow`) ) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.

theorem E8_norm_eq_sqrt_even (vFin 8 → ℝ : FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 8 → ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (hvv ∈ Submodule.E8 ℝ : vFin 8 → ℝ ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. Submodule.E8Submodule.E8.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule ℤ (Fin 8 → R) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  ∃ nℤ, EvenEven.{u_2} {α : Type u_2} [Add α] (a : α) : PropAn element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`,
for some `r : α`.  nℤ ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`). ↑nℤ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. WithLp.toLpWithLp.toLp.{u_1} (p : ENNReal) {V : Type u_1} (ofLp : V) : WithLp p VConverts an element of `V` to an element of `WithLp p V`.  2 vFin 8 → ℝ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2

theorem instDiscreteE8Lattice :
  DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  ↥E8LatticeE8Lattice : Submodule ℤ (EuclideanSpace ℝ (Fin 8))

theorem instIsZLatticeE8Lattice :
  IsZLatticeIsZLattice.{u_1, u_2} (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E]
  (L : Submodule ℤ E) [DiscreteTopology ↥L] : Prop`L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if
it is discrete and spans `E` over `K`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  E8LatticeE8Lattice : Submodule ℤ (EuclideanSpace ℝ (Fin 8))

theorem E8Basis_volume :
  MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
      (ZSpan.fundamentalDomainZSpan.fundamentalDomain.{u_1, u_2, u_3} {E : Type u_1} {ι : Type u_2} {K : Type u_3} [NormedField K]
  [NormedAddCommGroup E] [NormedSpace K E] (b : Module.Basis ι K E) [LinearOrder K] : Set EThe fundamental domain of the ℤ-lattice spanned by `b`. See `ZSpan.isAddFundamentalDomain`
for the proof that it is a fundamental domain. 
        (E8BasisE8Basis.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Module.Basis (Fin 8) R (Fin 8 → R) ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    1

theorem E8Packing_density :
  E8PackingE8Packing : PeriodicSpherePacking 8.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    ENNReal.ofRealENNReal.ofReal (r : ℝ) : ENNReal`ofReal x` returns `x` if it is nonnegative, `0` otherwise.  Real.piReal.pi : ℝThe number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2],
from which one can derive all its properties. For explicit bounds on π,
see `Mathlib/Analysis/Real/Pi/Bounds.lean`.

Denoted `π`, once the `Real` namespace is opened.  ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 4 /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. 384