  21variable {α : Type*} [Semiring α] [Star α]
  22
  23/-- A matrix is **unitary** if it is both a left- and right-inverse of its conjugate transpose. -/
  24def IsUnitary (U : Matrix m m α) : Prop :=
  25  U.conjTranspose * U = 1 ∧ U * U.conjTranspose = 1
  26
  27/-- A matrix is **normal** if it commutes with its conjugate transpose. -/
  28def IsNormal (U : Matrix m m α) : Prop :=
  29  U.conjTranspose * U = U * U.conjTranspose
  30
  31theorem IsUnitary.isNormal {U : Matrix m m α} (h : IsUnitary U) : IsNormal U := by
  32  unfold IsNormal
  33  rw [h.1, h.2]
  34
  35end Matrix

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.