Theorems · Theorem · functional analysis

Unitization.splitMul_injective_of_clm_mul_injective

∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A],
  Function.Injective ⇑(ContinuousLinearMap.mul 𝕜 A) → Function.Injective ⇑(Unitization.splitMul 𝕜 A)

this lemma establishes that if ContinuousLinearMap.mul 𝕜 A is injective, then so is Unitization.splitMul 𝕜 A. When A is a RegularNormedAlgebra, then ContinuousLinearMap.mul 𝕜 A is an isometry, and is therefore automatically injective.

Defined in

Mathlib.Analysis.Normed.Algebra.Unitization

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalNormedRingNormedSpaceIsScalarTowerSMulCommClass