Theorems · Definition · number theory

ZLattice.comap

(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] → Submodule ℤ E → (F →ₗ[K] E) → Submodule ℤ F

Let e : E → F a linear map, the map that sends a L : Submodule ℤ E to the Submodule ℤ F that is the pullback of L by e. If IsZLattice L and e is a continuous linear equiv, then it is a IsZLattice of E, see instIsZLatticeComap.

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace