theorem SpherePacking.finiteDensity_le {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (SSpherePacking d : SpherePackingSpherePacking (d : ℕ) : Type dℕ) (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ)
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  SSpherePacking d.finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal Rℝ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    ↑(Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.SSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.
              Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0
                (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.Rℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
                  SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ /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`.
                    2)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
          (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0
            (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`.SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ /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`. 2)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`.) /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`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)

theorem SpherePacking.finiteDensity_ge {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (SSpherePacking d : SpherePackingSpherePacking (d : ℕ) : Type dℕ) (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ)
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  SSpherePacking d.finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal Rℝ ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).
    ↑(Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.SSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.
              Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0
                (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).Rℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
                  SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ /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`.
                    2)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
          (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0
            (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`.SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ /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`. 2)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`.) /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`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)

theorem PeriodicSpherePacking.aux2_ge'.{u_1}
  {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (SPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ)
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1] {Lℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (bModule.Basis ι ℤ ↥S.lattice : Module.BasisModule.Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 ιType u_1 ℤ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).
 ↥SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)))
  (hL∀ x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L :
    ∀
      xEuclideanSpace ℝ (Fin d) ∈
        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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Lℝ)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) :
  ↑(Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.↑SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).
    MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).Rℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). Lℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).) /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`.
      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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice))

theorem PeriodicSpherePacking.aux2_le'.{u_1}
  {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (SPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ)
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1] {Lℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. )
  (bModule.Basis ι ℤ ↥S.lattice : Module.BasisModule.Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 ιType u_1 ℤ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).
 ↥SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)))
  (hL∀ x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L :
    ∀
      xEuclideanSpace ℝ (Fin d) ∈
        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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Lℝ)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) :
  ↑(Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.↑SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.Rℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. Lℝ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.) /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`.
      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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice))

theorem PeriodicSpherePacking.aux_ge.{u_1} {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (SPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1]
  (bModule.Basis ι ℤ ↥S.lattice : Module.BasisModule.Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 ιType u_1 ℤ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).
 ↥SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)))
  {Lℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (hL∀ x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L :
    ∀
      xEuclideanSpace ℝ (Fin d) ∈
        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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Lℝ)
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  (Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.SPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).
    SPeriodicSpherePacking d.numRepsPeriodicSpherePacking.numReps {d : ℕ} (S : PeriodicSpherePacking d) : ℕ •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      (Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.↑SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.
          Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).Rℝ -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). Lℝ)HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞` 

theorem PeriodicSpherePacking.aux_le.{u_1} {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  (SPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_1]
  (bModule.Basis ι ℤ ↥S.lattice : Module.BasisModule.Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 ιType u_1 ℤ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).
 ↥SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)))
  {Lℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (hL∀ x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L :
    ∀
      xEuclideanSpace ℝ (Fin d) ∈
        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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Lℝ)
  (Rℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. ) :
  (Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.SPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 Rℝ)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞`  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    SPeriodicSpherePacking d.numRepsPeriodicSpherePacking.numReps {d : ℕ} (S : PeriodicSpherePacking d) : ℕ •HSMul.hSMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSMul α β γ] : α → β → γ`a • b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent, but it is intended to be used for left actions. 

Conventions for notations in identifiers:

 * The recommended spelling of `•` in identifiers is `smul`.
      (Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.↑SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) ∩Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`.
          Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.Rℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. Lℝ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.)Inter.inter.{u} {α : Type u} [self : Inter α] : α → α → α`a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`..encardSet.encard.{u_1} {α : Type u_1} (s : Set α) : ℕ∞The cardinality of a set as a term in `ℕ∞` 

theorem volume_ball_ratio_tendsto_nhds_one''
  {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} {Cℝ C'ℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. } (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) :
  Filter.TendstoFilter.Tendsto.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Prop`Filter.Tendsto` is the generic "limit of a function" predicate.
`Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
the `f`-preimage of `a` is an `l₁` neighborhood. 
    (fun Rℝ ↦
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
          (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.Rℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. Cℝ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.) /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`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
          (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.Rℝ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. C'ℝ)HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.))
    Filter.atTopFilter.atTop.{u_3} {α : Type u_3} [Preorder α] : Filter α`atTop` is the filter representing the limit `→ ∞` on an ordered set.
It is generated by the collection of up-sets `{b | a ≤ b}`.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)  (nhdsnhds.{u_3} {X : Type u_3} [TopologicalSpace X] (x : X) : Filter XA set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.  1)

theorem PeriodicSpherePacking.density_eq.{u_3}
  {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} {SPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ}
  {ιType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 ιType u_3]
  (bModule.Basis ι ℤ ↥S.lattice : Module.BasisModule.Basis.{u_1, u_3, u_6} (ι : Type u_1) (R : Type u_3) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] :
  Type (max (max u_1 u_3) u_6)A `Basis ι R M` for a module `M` is the type of `ι`-indexed `R`-bases of `M`.

The basis vectors are available as `DFunLike.coe (b : Basis ι R M) : ι → M`.
To turn a linear independent family of vectors spanning `M` into a basis, use `Basis.mk`.
They are internally represented as linear equivs `M ≃ₗ[R] (ι →₀ R)`,
available as `Basis.repr`.
 ιType u_3 ℤ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).
 ↥SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)))
  {Lℝ : ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. }
  (hL∀ x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ S.lattice b), ‖x‖ ≤ L :
    ∀
      xEuclideanSpace ℝ (Fin d) ∈
        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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). Lℝ)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) :
  SPeriodicSpherePacking d.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`.
    ↑SPeriodicSpherePacking d.numRepsPeriodicSpherePacking.numReps {d : ℕ} (S : PeriodicSpherePacking d) : ℕ *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
          (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0
            (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`.SPeriodicSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ /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`. 2)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`.) /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`.
      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. 
          (Module.Basis.ofZLatticeBasisModule.Basis.ofZLatticeBasis.{u_1, u_2, u_3} (K : Type u_1) [NormedField K] [LinearOrder K] [IsStrictOrderedRing K]
  [HasSolidNorm K] [FloorRing K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E]
  [ProperSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] {ι : Type u_3} [hs : IsZLattice K L]
  (b : Module.Basis ι ℤ ↥L) : Module.Basis ι K EAny `ℤ`-basis of `L` is also a `K`-basis of `E`.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers. 
            SPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) bModule.Basis ι ℤ ↥S.lattice))