conjTranspose_eq_transpose_of_trivial

English

If the star operation is trivial (star x = x for all x), then conjugate transpose coincides with the ordinary transpose: A^H = A^T.

Русский

Если операция звезды тривиальна (star x = x), то сопряжённое транспонирование совпадает с обычным транспонированием: A^H = A^T.

LaTeX

$$$ A^H = A^T $$$

Lean4

/-- When `star x = x` on the coefficients (such as the real numbers) `conjTranspose` and `transpose`
are the same operation. -/
@[simp]
theorem conjTranspose_eq_transpose_of_trivial [Star α] [TrivialStar α] (A : Matrix m n α) : Aᴴ = Aᵀ :=
  Matrix.ext fun _ _ => star_trivial _

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