toCLM_injective — Mathlib

English

The map toCLM is injective; distinct matrices give distinct continuous linear maps.

Русский

Карта toCLM инъективна; различные матрицы соответствуют различным непрерывно линейным отображениям.

LaTeX

$$toCLM is injective$$

Lean4

theorem toCLM_injective : Function.Injective (toCLM (A := A) (m := m) (n := n)) := by
  classical
  rw [injective_iff_map_eq_zero]
  intro M h
  ext i j
  rw [Matrix.zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self, ←
    toCLM_apply_single_apply]
  simp [h]

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