Theorems · Theorem · functional analysis

ContinuousMultilinearMap.toMultilinearMapLinear_apply

∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {R' : Type u_1} {A : Type u_2} [inst : Semiring R']
  [inst_1 : Semiring A] [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : (i : ι) → TopologicalSpace (M₁ i)] [inst_5 : TopologicalSpace M₂] [inst_6 : ContinuousAdd M₂]
  [inst_7 : (i : ι) → Module A (M₁ i)] [inst_8 : Module A M₂] [inst_9 : Module R' M₂]
  [inst_10 : ContinuousConstSMul R' M₂] [inst_11 : SMulCommClass A R' M₂] (self : ContinuousMultilinearMap A M₁ M₂),
  ContinuousMultilinearMap.toMultilinearMapLinear self = self.toMultilinearMap

Defined in

Mathlib.Topology.Algebra.Module.Multilinear.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidAddCommMonoidTopologicalSpaceTopologicalSpaceContinuousAddModuleModuleModuleContinuousConstSMulSMulCommClass