Theorems · Definition · number theory

Module.Basis.ofZLatticeBasis

(K : Type u_1) →
  [inst : NormedField K] →
    [inst_1 : LinearOrder K] →
      [IsStrictOrderedRing K] →
        [HasSolidNorm K] →
          [FloorRing K] →
            {E : Type u_2} →
              [inst_5 : NormedAddCommGroup E] →
                [inst_6 : NormedSpace K E] →
                  [FiniteDimensional K E] →
                    [ProperSpace E] →
                      (L : Submodule ℤ E) →
                        [inst_9 : DiscreteTopology ↥L] →
                          {ι : Type u_3} → [hs : IsZLattice K L] → Module.Basis ι ℤ ↥L → Module.Basis ι K E

Any ℤ-basis of L is also a K-basis of E.

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

36 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldLinearOrderIsStrictOrderedRingHasSolidNormFloorRingNormedAddCommGroupNormedSpaceFiniteDimensionalProperSpaceDiscreteTopologyIsZLattice