conjTranspose_eq_natCast — Mathlib

English

Let M be n×n and d a natural number. Then M^H equals d.cast if and only if M equals d.cast.

Русский

Пусть M — n×n матрица, и d — натуральное число. Тогда M^H = d.cast тогда и только тогда, когда M = d.cast.

LaTeX

$$$M^{H} = d. cast \iff M = d.cast$$$

Lean4

@[simp]
theorem conjTranspose_eq_natCast [DecidableEq n] [NonAssocSemiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} :
    Mᴴ = d ↔ M = d :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <| by rw [conjTranspose_natCast]

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