Theorems · Theorem · functional analysis

ContinuousLinearMap.opNNNorm_mul

∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalNormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R]
  [Nontrivial R], ‖ContinuousLinearMap.mul 𝕜 R‖₊ = 1

Defined in: Mathlib.Analysis.Normed.Operator.Mul
Cited by: 1 results in Mathlib
Foundations: Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField NonUnitalNormedRing NormedSpace IsScalarTower SMulCommClass RegularNormedAlgebra Nontrivial

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement · cited by 18,349
NormedSpacestatement and proof · cited by 12,499
NontriviallyNormedFieldstatement and proof · cited by 8,742
ContinuousLinearMapstatement · cited by 5,352
NNRealstatement · cited by 4,310
IsScalarTowerstatement and proof · cited by 3,896
Nontrivialstatement and proof · cited by 2,416
SMulCommClassstatement and proof · cited by 1,927
NNNorm.nnnormstatement · cited by 952
NonUnitalNormedRingstatement and proof · cited by 231
ContinuousLinearMap.mulstatement · cited by 63
RegularNormedAlgebrastatement and proof · cited by 26

Cited by1

Results whose statement or proof uses this declaration.

ContinuousLinearMap.opENorm_mulproof · cited by 0