Evaluating star of a matrix

Stream: new members

[Maris Ozols]

I'm trying to prove that a simple 3x3 matrix is untary but for some reason the last rewrite with star_apply doesn't work.

import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Data.Complex.Basic

open Matrix

abbrev U3 := unitaryGroup (Fin 3) ℂ

def X : Matrix (Fin 3) (Fin 3) ℂ :=
  !![ 0, 0, 1;
      1, 0, 0;
      0, 1, 0 ]

lemma X_in_U3 : X ∈ U3 := by
  rw [mem_unitaryGroup_iff]
  unfold X
  ext i j
  rw [mul_apply]
  rw [star_apply]
  sorry

[Ruben Van de Velde]

That's because it's under the sum. simp_rw works

[Maris Ozols]

Any tips on how to finish this proof or how to do these types of proofs that involve simple calculations with small explicit numerical matrices?

[Kenny Lau]

norm_num

[Kenny Lau]

oh wait, it's matrices, sorry

[Kenny Lau]

you need to split it into nine goals (one for each component) first, and then do norm_num

[Kenny Lau]

someone asked a similar question and i forgot the answer...

[Kenny Lau]

import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Data.Complex.Basic

open Matrix

abbrev U3 := unitaryGroup (Fin 3) ℂ

def X : Matrix (Fin 3) (Fin 3) ℂ :=
  !![ 0, 0, 1;
      1, 0, 0;
      0, 1, 0 ]

lemma X_in_U3 : X ∈ U3 := by
  have star_X_eq : star X =
      !![star 0, star 1, star 0; star 0, star 0, star 1; star 1, star 0, star 0] :=
    Matrix.etaExpand_eq _ |>.symm
  rw [mem_unitaryGroup_iff, star_X_eq, X]
  ext i j; fin_cases i <;> fin_cases j <;> simp

[Kenny Lau]

@Eric Wieser might have more to say on this

[Eric Wieser]

I think we're missing some automation to transpose concrete matrices

[Kenny Lau]

import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Data.Complex.Basic

open Matrix

abbrev U3 := unitaryGroup (Fin 3) ℂ

def X : Matrix (Fin 3) (Fin 3) ℂ :=
  !![ 0, 0, 1;
      1, 0, 0;
      0, 1, 0 ]

lemma X_in_U3 : X ∈ U3 := by
  rw [mem_unitaryGroup_iff, X]
  ext i j; fin_cases i <;> fin_cases j <;>
  simp [Matrix.vecMul_eq_sum, Fin.sum_univ_three]