IsNormal
plain-language theorem explainer
The definition states that a matrix is normal precisely when it commutes with its conjugate transpose. Workers on linear-algebraic support layers inside Recognition Science would cite the predicate for cross-Mathlib stability. The declaration is a direct equality with no lemmas or tactics required.
Claim. A matrix $U$ is normal when $U^*U = UU^*$, where $*$ denotes the conjugate transpose.
background
The module supplies lightweight, project-local predicates for unitary and normal matrices to remain stable across Mathlib versions. Unitary requires both $U^U=I$ and $UU^=I$. Normal requires commutativity of the matrix with its conjugate transpose. The module documentation presents these as the standard algebraic definitions. The two upstream U declarations supply RS-native units and a recognition structure but are not referenced inside the matrix predicates themselves.
proof idea
The declaration is the direct definition of the normal property via the equality between the two products. No lemmas are applied and no tactics are used; it is an abbrev-style definition.
why it matters
The predicate is referenced by the sibling IsUnitary definition and by the theorem that every unitary matrix is normal. It supplies stable infrastructure for matrix arguments inside the support module. No link to the forcing chain T0-T8 or the Recognition Composition Law is present; the definition remains auxiliary linear-algebra tooling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.