conjTranspose_pow — Mathlib

English

Conjugate transpose commutes with taking powers: the H-transpose of M^k equals (M^H)^k for square M under semiring and star, with finite type assumptions.

Русский

Сопряжённое транспонирование commute с возведением в степень: (M^k)^H = (M^H)^k для квадратной M при соответствующих условиях.

LaTeX

$$$ (M^k)^H = (M^H)^k $$$

Lean4

@[simp]
theorem conjTranspose_pow [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (M : Matrix m m α) (k : ℕ) :
    (M ^ k)ᴴ = Mᴴ ^ k :=
  MulOpposite.op_injective <| map_pow (conjTransposeRingEquiv m α) M k

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