Theorems · Theorem · functional analysis

LinearIsometryEquiv.submoduleMap_apply_coe

∀ {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : SeminormedAddCommGroup M] [inst_3 : SeminormedAddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M)
  (e : M ≃ₛₗᵢ[σ₁₂] M₂) (c : ↥p), ↑((LinearIsometryEquiv.submoduleMap p e) c) = e ↑c

Defined in

Mathlib.Analysis.Normed.Operator.LinearIsometry

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingRingSeminormedAddCommGroupSeminormedAddCommGroupModuleModule