Theorems · Theorem · number theory

Module.Basis.ofZLatticeComap_apply

∀ (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} (b : Module.Basis ι ℤ ↥L) (i : ι),
  ↑((Module.Basis.ofZLatticeComap K L e b) i) = e.symm ↑(b i)

Defined in

Mathlib.Algebra.Module.ZLattice.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace