Theorems · Theorem · functional analysis

enorm_smul

∀ {α : Type u_1} {β : Type u_2} [inst : ENorm α] [inst_1 : ENorm β] [inst_2 : SMul α β] [ENormSMulClass α β] (r : α)
  (x : β), ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Defined in

Mathlib.Analysis.Normed.MulAction

Cited by

14 results in Mathlib

Foundations

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

Assumes

ENormENormSMulENormSMulClass