Results about operator norms in normed algebras

This file (split off from OperatorNorm.lean) contains results about the operator norm of multiplication and scalar-multiplication operations in normed algebras and normed modules.

noncomputable def ContinuousLinearMap.mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a non-unital normed algebra as a continuous bilinear map.

Equations

• ContinuousLinearMap.mul 𝕜 𝕜' = (LinearMap.mul 𝕜 𝕜').mkContinuous₂ 1 ⋯

@[simp]

theorem ContinuousLinearMap.mul_apply' (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') : ((ContinuousLinearMap.mul 𝕜 𝕜') x) y = x * y

@[simp]

theorem ContinuousLinearMap.opNorm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ ≤ ‖x‖

@[deprecated ContinuousLinearMap.opNorm_mul_apply_le]

theorem ContinuousLinearMap.op_norm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ ≤ ‖x‖

Alias of ContinuousLinearMap.opNorm_mul_apply_le.

theorem ContinuousLinearMap.opNorm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ ≤ 1

@[deprecated ContinuousLinearMap.opNorm_mul_le]

theorem ContinuousLinearMap.op_norm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ ≤ 1

Alias of ContinuousLinearMap.opNorm_mul_le.

noncomputable def NonUnitalAlgHom.Lmul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →ₙₐ[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication on the left in a non-unital normed algebra 𝕜' as a non-unital algebra homomorphism into the algebra of continuous linear maps. This is the left regular representation of A acting on itself.

This has more algebraic structure than ContinuousLinearMap.mul, but there is no longer continuity bundled in the first coordinate. An alternative viewpoint is that this upgrades NonUnitalAlgHom.lmul from a homomorphism into linear maps to a homomorphism into continuous linear maps.

Equations

• NonUnitalAlgHom.Lmul 𝕜 𝕜' = let __src := ContinuousLinearMap.mul 𝕜 𝕜'; { toFun := (↑__src).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.coe_Lmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_3} [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ⇑(NonUnitalAlgHom.Lmul 𝕜 𝕜') = ⇑(ContinuousLinearMap.mul 𝕜 𝕜')

noncomputable def ContinuousLinearMap.mulLeftRight (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜'

Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a continuous trilinear map. This is akin to its non-continuous version LinearMap.mulLeftRight, but there is a minor difference: LinearMap.mulLeftRight is uncurried.

Equations

• ContinuousLinearMap.mulLeftRight 𝕜 𝕜' = ((ContinuousLinearMap.compL 𝕜 𝕜' 𝕜' 𝕜').comp (ContinuousLinearMap.mul 𝕜 𝕜').flip).flip.comp (ContinuousLinearMap.mul 𝕜 𝕜')

@[simp]

theorem ContinuousLinearMap.mulLeftRight_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') (z : 𝕜') : (((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y) z = x * z * y

theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') : ‖((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y‖ ≤ ‖x‖ * ‖y‖

@[deprecated ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le]

theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') (y : 𝕜') : ‖((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y‖ ≤ ‖x‖ * ‖y‖

Alias of ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le.

theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x‖ ≤ ‖x‖

@[deprecated ContinuousLinearMap.opNorm_mulLeftRight_apply_le]

theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x‖ ≤ ‖x‖

Alias of ContinuousLinearMap.opNorm_mulLeftRight_apply_le.

theorem ContinuousLinearMap.opNorm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mulLeftRight 𝕜 𝕜'‖ ≤ 1

@[deprecated ContinuousLinearMap.opNorm_mulLeftRight_le]

theorem ContinuousLinearMap.op_norm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : ‖ContinuousLinearMap.mulLeftRight 𝕜 𝕜'‖ ≤ 1

Alias of ContinuousLinearMap.opNorm_mulLeftRight_le.

class RegularNormedAlgebra (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] : Prop

This is a mixin class for non-unital normed algebras which states that the left-regular representation of the algebra on itself is isometric. Every unital normed algebra with ‖1‖ = 1 is a regular normed algebra (see NormedAlgebra.instRegularNormedAlgebra). In addition, so is every C⋆-algebra, non-unital included (see CstarRing.instRegularNormedAlgebra), but there are yet other examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regular.

This is a useful class because it gives rise to a nice norm on the unitization; in particular it is a C⋆-norm when the norm on A is a C⋆-norm.

• isometry_mul' : Isometry ⇑(ContinuousLinearMap.mul 𝕜 𝕜')

  The left regular representation of the algebra on itself is an isometry.

theorem RegularNormedAlgebra.isometry_mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {𝕜' : Type u_3} [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [self : RegularNormedAlgebra 𝕜 𝕜'] : Isometry ⇑(ContinuousLinearMap.mul 𝕜 𝕜')

The left regular representation of the algebra on itself is an isometry.

noncomputable instance NormedAlgebra.instRegularNormedAlgebra {𝕜 : Type u_4} {𝕜' : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] : RegularNormedAlgebra 𝕜 𝕜'

Every (unital) normed algebra such that ‖1‖ = 1 is a RegularNormedAlgebra.

Equations

• ⋯ = ⋯

theorem ContinuousLinearMap.isometry_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : Isometry ⇑(ContinuousLinearMap.mul 𝕜 𝕜')

@[simp]

theorem ContinuousLinearMap.opNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ = ‖x‖

@[deprecated ContinuousLinearMap.opNorm_mul_apply]

theorem ContinuousLinearMap.op_norm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ = ‖x‖

Alias of ContinuousLinearMap.opNorm_mul_apply.

@[simp]

theorem ContinuousLinearMap.opNNNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖₊ = ‖x‖₊

@[deprecated ContinuousLinearMap.opNNNorm_mul_apply]

theorem ContinuousLinearMap.op_nnnorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] (x : 𝕜') : ‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖₊ = ‖x‖₊

Alias of ContinuousLinearMap.opNNNorm_mul_apply.

noncomputable def ContinuousLinearMap.mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜'

Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.

Equations

• ContinuousLinearMap.mulₗᵢ 𝕜 𝕜' = { toLinearMap := ↑(ContinuousLinearMap.mul 𝕜 𝕜'), norm_map' := ⋯ }

@[simp]

theorem ContinuousLinearMap.coe_mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalSeminormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] : ⇑(ContinuousLinearMap.mulₗᵢ 𝕜 𝕜') = ⇑(ContinuousLinearMap.mul 𝕜 𝕜')

noncomputable def ContinuousLinearMap.ring_lmap_equiv_selfₗ (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E

If M is a normed space over 𝕜, then the space of maps 𝕜 →L[𝕜] M is linearly equivalent to M. (See ring_lmap_equiv_self for a stronger statement.)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContinuousLinearMap.ring_lmap_equiv_self (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E

If M is a normed space over 𝕜, then the space of maps 𝕜 →L[𝕜] M is linearly isometrically equivalent to M.

Equations

• ContinuousLinearMap.ring_lmap_equiv_self 𝕜 E = { toLinearEquiv := ContinuousLinearMap.ring_lmap_equiv_selfₗ 𝕜 E, norm_map' := ⋯ }

noncomputable def ContinuousLinearMap.lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : 𝕜' →L[𝕜] E →L[𝕜] E

Scalar multiplication as a continuous bilinear map.

Equations

• ContinuousLinearMap.lsmul 𝕜 𝕜' = (Algebra.lsmul 𝕜 𝕜 E).toLinearMap.mkContinuous₂ 1 ⋯

@[simp]

theorem ContinuousLinearMap.lsmul_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (c : 𝕜') (x : E) : ((ContinuousLinearMap.lsmul 𝕜 𝕜') c) x = c • x

theorem ContinuousLinearMap.norm_toSpanSingleton (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖ContinuousLinearMap.toSpanSingleton 𝕜 x‖ = ‖x‖

theorem ContinuousLinearMap.opNorm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (x : 𝕜') : ‖(ContinuousLinearMap.lsmul 𝕜 𝕜') x‖ ≤ ‖x‖

@[deprecated ContinuousLinearMap.opNorm_lsmul_apply_le]

theorem ContinuousLinearMap.op_norm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] (x : 𝕜') : ‖(ContinuousLinearMap.lsmul 𝕜 𝕜') x‖ ≤ ‖x‖

Alias of ContinuousLinearMap.opNorm_lsmul_apply_le.

theorem ContinuousLinearMap.opNorm_lsmul_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ ≤ 1

The norm of lsmul is at most 1 in any semi-normed group.

@[deprecated ContinuousLinearMap.opNorm_lsmul_le]

theorem ContinuousLinearMap.op_norm_lsmul_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {𝕜' : Type u_3} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ ≤ 1

Alias of ContinuousLinearMap.opNorm_lsmul_le.

---

The norm of lsmul is at most 1 in any semi-normed group.

@[simp]

theorem ContinuousLinearMap.opNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ = 1

@[deprecated ContinuousLinearMap.opNorm_mul]

theorem ContinuousLinearMap.op_norm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖ = 1

Alias of ContinuousLinearMap.opNorm_mul.

@[simp]

theorem ContinuousLinearMap.opNNNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖₊ = 1

@[deprecated ContinuousLinearMap.opNNNorm_mul]

theorem ContinuousLinearMap.op_nnnorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (𝕜' : Type u_3) [NonUnitalNormedRing 𝕜'] [NormedSpace 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' 𝕜'] [SMulCommClass 𝕜 𝕜' 𝕜'] [RegularNormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] : ‖ContinuousLinearMap.mul 𝕜 𝕜'‖₊ = 1

Alias of ContinuousLinearMap.opNNNorm_mul.

@[simp]

theorem ContinuousLinearMap.opNorm_lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ = 1

The norm of lsmul equals 1 in any nontrivial normed group.

This is ContinuousLinearMap.opNorm_lsmul_le as an equality.

@[deprecated ContinuousLinearMap.opNorm_lsmul]

theorem ContinuousLinearMap.op_norm_lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (𝕜' : Type u_3) [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Nontrivial E] : ‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ = 1

Alias of ContinuousLinearMap.opNorm_lsmul.

---

The norm of lsmul equals 1 in any nontrivial normed group.

This is ContinuousLinearMap.opNorm_lsmul_le as an equality.