conjTranspose_injective — Mathlib

English

If α has an involutive star, the map A ↦ A^H is injective: A^H = B^H implies A = B.

Русский

Если звезда на α — инвольютивна, отображение A ↦ A^H инъективно: A^H = B^H => A = B.

LaTeX

$$$\text{conjTranspose}: M^{n\times m}(\alpha) \to M^{m\times n}(\alpha)$ is injective, i.e., A^H = B^H \Rightarrow A = B$$$

Lean4

theorem conjTranspose_injective [InvolutiveStar α] : Function.Injective (conjTranspose : Matrix m n α → Matrix n m α) :=
  (map_injective star_injective).comp transpose_injective

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