IsNormal
plain-language theorem explainer
The IsNormal definition encodes the algebraic condition that a square matrix commutes with its conjugate transpose. Matrix theorists cite this predicate when classifying operators that satisfy the normality relation in finite dimensions. It is supplied as a direct equality to ensure stability across Mathlib versions.
Claim. A matrix $U$ over a field is normal when $U^* U = U U^*$, where $^*$ denotes the conjugate transpose.
background
The module supplies project-local predicates for unitary and normal matrices to avoid version differences in Mathlib. Unitary requires both $U^* U = 1$ and $U U^* = 1$. Normal requires the commutation $U^* U = U U^*$ as stated in the module documentation.
proof idea
Direct definition consisting of the single equality between the two orderings of the matrix and its conjugate transpose.
why it matters
This definition supports the sibling result that every unitary matrix is normal. It supplies a stable algebraic predicate for matrix manipulations required in the Recognition framework without invoking the J-cost, phi-ladder, or forcing chain steps T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.