Theorems · Inductive type · combinatorics

Matrix.IsHadamard

{n : Type u_2} →
  {R : Type u_3} → [Fintype n] → [DecidableEq n] → [inst : Semiring R] → [StarRing R] → Matrix n n R → Prop

A square matrix over a *-semiring whose entries are unitary and whose rows and columns are orthogonal with respect to the conjugate transpose: A * Aᴴ = n • 1 and Aᴴ * A = n • 1. Over a commutative ring in which the order is regular, the one-sided condition from [Definition 2.3.1][deLauneyFlannery2011] implies this predicate by IsHadamard.of_mul_conjTranspose; over a ring with trivial star (e.g. ℝ, ℤ), the entry condition becomes A i j = 1 ∨ A i j = -1. Over ℂ, the entry condition becomes ‖A i j‖ = 1, generalizing the fourth-root complex Hadamard matrices of [Definition 2.7.1][deLauneyFlannery2011].

Defined in

Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Cited by

24 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

FintypeDecidableEqSemiringStarRing