splitMul_injective — Mathlib

English

Under RegularNormedAlgebra 𝕜 A, the map splitMul 𝕜 A is injective.

Русский

При RegularNormedAlgebra 𝕜 A отображение splitMul 𝕜 A инъективно.

LaTeX

$$$$\\text{Injective}(splitMul\\ 𝕜 A).$$$$

Lean4

/-- In a `RegularNormedAlgebra`, the map `Unitization.splitMul 𝕜 A` is injective.
We will use this to pull back the norm from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A`. -/
theorem splitMul_injective : Function.Injective (splitMul 𝕜 A) :=
  splitMul_injective_of_clm_mul_injective (isometry_mul 𝕜 A).injective

Похожие утверждения