Theorems · Definition · number theory

Module.Basis.ofZLatticeComap

(K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace K F] →
                (L : Submodule ℤ E) →
                  (e : F ≃ₗ[K] E) → {ι : Type u_4} → Module.Basis ι ℤ ↥L → Module.Basis ι ℤ ↥(ZLattice.comap K L ↑e)

The basis of ZLattice.comap K L e given by the image of a basis b of L by e.symm.

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace