Documentation

LeanPool.HopfProblem.Lattice.Core2

Hopf problem: lattice · core 2 #

Supporting definitions and proofs for this stage of the six-sphere construction.

source
@[reducible, inline]
abbrev Mathoverflow1973.LocalSystemMatrices.Vec (n : ℕ) :
Type

An integer coordinate vector of length n.

Equations
Instances For
    source
    def Mathoverflow1973.LocalSystemMatrices.lastCoordinate :
    Vec 4 →ₗ[ℤ] ℤ

    The linear functional selecting the last coordinate of a rank-four vector.

    Equations
    Instances For
      source
      def Mathoverflow1973.LocalSystemMatrices.pairIndices :
      Fin 6 → Fin 2 → Fin 4

      The two coordinate indices represented by an exterior-square basis element.

      Equations
      Instances For