Define a normalized complex vector.

Stream: new members

[Yunong Shi]

I want to define a normalized vector using Mathlib, and I expected the following to work

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

structure normalized_complex_vector (d: Nat) where
  v: Matrix (Fin d) (Fin 1) ℂ
  norm: v * vᴴ = 1

However, Lean complains that it fails to synthesize instances for v * vᴴ = 1. What is the problem?

The error message is:

failed to synthesize instance
  HMul (Matrix (Fin d) (Fin 1) ℂ) (Matrix (Fin d) (Fin 1) ℂ) ?m.31529

[Martin Dvořák]

Seems you need to either transpose a matrix, or use a vector and something like dotProduct.

[Yunong Shi]

Martin Dvořák said:

Seems you need to either transpose a matrix, or use a vector and something like dotProduct.

I thought that I conjugate transposed the 2nd v with ᴴ, is that right?

[Martin Dvořák]

Can you give me the right import so that I will be able to check?

[Yunong Shi]

Martin Dvořák said:

Can you give me the right import so that I will be able to check?

Here it is

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

I also add it to the main post.

[Martin Dvořák]

Interesting this works:

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

structure normalized_complex_vector (d: Nat) where
  v: Matrix (Fin d) (Fin 1) ℂ
  norm: v * v.conjTranspose = 1

[Yunong Shi]

Martin Dvořák said:

Interesting this works:

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

structure normalized_complex_vector (d: Nat) where
  v: Matrix (Fin d) (Fin 1) ℂ
  norm: v * v.conjTranspose = 1

ah... That is indeed very interesting...

[Martin Dvořák]

open Matrix

[Yunong Shi]

Martin Dvořák said:

open Matrix

Thanks! I guess that I need to strengthen my understanding of scopes now.

[Martin Dvořák]

I'd like to know how it originally understood ᴴ so that it complained about * instead. Maybe it was trying to parse (v * v)ᴴ before opening the scope which revealed the priority of the notation.

[Eric Wieser]

It is complaining about both errors simultaneously

[Eric Wieser]

open scoped Matrix is probably safer than open Matrix

[Martin Dvořák]

Is ?m.31529 about the unknown symbol?

[Kevin Buzzard]

That's lean saying "multiplication is heterogeneous but I can't find any * which eats two d x 1 matrices and spits out anything at all"