Theorems · Definition · number theory

ZLattice.comap_equiv

(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) → ↥L ≃ₗ[ℤ] ↥(ZLattice.comap K L ↑e)

If e is a linear equivalence, it induces a ℤ-linear equivalence between L and ZLattice.comap K L e.

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace