matrix

Stream: mathlib4

[BANGJI HU]

I tried to calculate the fourth power of this matrix but the result seem !![Real.ofCauchy (sorry /- 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I,
Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- -8, -8, -8, -8, -8, -8, -8, -8, -8, -8, ... -/)*I;
Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/) + Real.ofCauchy (sorry /- 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, ... -/)*I,
Real.ofCauchy (sorry /- 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, ... -/) + Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)*I]

import Mathlib
open Matrix Complex


def sigma_y : Matrix (Fin 2) (Fin 2) ℂ :=
  ![
    ![1, -I],
    ![I, 1]
  ]

#eval (sigma_y^ 4)

[Jeremy Tan]

import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Mul
import Mathlib.Tactic.FinCases

open Complex Matrix

def pauli₁ : Matrix (Fin 2) (Fin 2) ℂ := ![![0, 1], ![1, 0]]
def pauli₂ : Matrix (Fin 2) (Fin 2) ℂ := ![![0, -I], ![I, 0]]
def pauli₃ : Matrix (Fin 2) (Fin 2) ℂ := ![![1, 0], ![0, -1]]

lemma pauli₂_sq : pauli₂ ^ 2 = 1 := by
  rw [pauli₂, sq]
  ext i j; fin_cases i <;> fin_cases j
  all_goals
    rw [mul_apply, Fin.sum_univ_two]
    simp

[BANGJI HU]

@Jeremy Tan take a look is ![
![1, -I],
![I, 1]
] a vector or matrix

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Basic
import Mathlib.Tactic

open Matrix Complex
theorem sigma_y_pow_four :
  ![
    ![1, -I],
    ![I, 1]
  ] ^ 4 = ![
    ![8 , -8 •I],
    ![8 •I, 8 ]
  ] := by


  fin_cases i <;> fin_cases j <;>
  all_goals
  simp [pow_succ, mul_apply, Fin.sum_univ_succ, Fin.sum_univ_zero]

[Eric Wieser]

You should use !![ for matrices, not ![![