Theorems · Theorem · functional analysis

isBoundedBilinearMap_smul

∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : SeminormedRing A] [inst_2 : Algebra 𝕜 A]
  {E : Type u_3} [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : Module A E] [IsBoundedSMul A E]
  [IsScalarTower 𝕜 A E], IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2

Scalar multiplication (for a normed 𝕜-algebra acting on a normed 𝕜-module) as a bounded bilinear map.

Defined in

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringSeminormedRingAlgebraSeminormedAddCommGroupModuleModuleIsBoundedSMulIsScalarTower