Scalar multiplication for unitary matrices

Stream: new members

[Maris Ozols]

I wonder if unitary matrices should support scalar multiplication, with result being a regular matrix. Here is a small example where scalar multiplication failed to synthesize HSMul ℂ ↥U3 ?m.6625:

import Mathlib.Analysis.SpecialFunctions.Complex.Log
import Mathlib.LinearAlgebra.UnitaryGroup

open Matrix Complex Real

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

-- Unitary group U(3)
abbrev U3 := unitaryGroup (Fin 3) ℂ

-- X is unitary
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]

-- Unitary version of X
def UX : U3 := ⟨X, X_in_U3⟩

-- Third root of unity
noncomputable def ω : ℂ := exp (2 * π * I / 3)

#check X * UX
#check UX * X
#check ω • X
#check ω • UX

Similarly, it would also be nice to have addition for unitary matrices since #check UX + UX also fails. Or should I just always write UX.1 to convert my unitary matrix to a regular matrix?

[Jireh Loreaux]

I would suggest to work with X most of the time and the predicate and only bundle into the subtype when necessary. You can even do the latter with the lift tactic.