def
definition
IsNormal
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Support.MatrixProperties on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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