IndisputableMonolith.Support.MatrixProperties

   1import Mathlib
   2
   3/-!
   4# Matrix Properties (Unitary / Normal)
   5
   6Mathlib versions can differ on whether `Matrix.IsUnitary` / `Matrix.IsNormal`
   7are available. This module defines lightweight, project-local predicates that
   8are stable across Mathlib versions.
   9
  10These are the standard algebraic definitions:
  11
  12- Unitary: \(U^\* U = I\) and \(U U^\* = I\)
  13- Normal: \(U^\* U = U U^\*\)
  14-/
  15
  16namespace Matrix
  17
  18open scoped Matrix
  19
  20variable {m : Type*} [Fintype m] [DecidableEq m]
  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
  36