LatticeBasis.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bases of full lattices

The finitely generated, rationally spanning submodules used in FullLattice are free of rank equal to the field degree. Their integer bases become rational bases without changing the underlying vectors.

def OAI.DukePrimeDegree.FullLattice.rationalBasis line 20
Source documentation
An integer basis of a full lattice is a rational basis of the field.
```
noncomputable def FullLattice.rationalBasis {ι : Type*} (M : FullLattice K)
    (b : Module.Basis ι ℤ M.toSubmodule) : Module.Basis ι ℚ K := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice
lemma OAI.DukePrimeDegree.FullLattice.rationalBasis_apply line 36
lemma OAI.DukePrimeDegree.FullLattice.finrank line 43
Source documentation
The rank in the manuscript's definition follows from finite generation and rational spanning; it is not an extra hypothesis.
```
lemma FullLattice.finrank (M : FullLattice K) :
    Module.finrank ℤ M.toSubmodule = Module.finrank ℚ K := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice
def OAI.DukePrimeDegree.FullLattice.integralBasis line 50
Source documentation
A full lattice has an integer basis indexed by the degree of the field.
```
noncomputable def FullLattice.integralBasis (M : FullLattice K) :
    Module.Basis (Fin (Module.finrank ℚ K)) ℤ M.toSubmodule := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice