Theorems · Theorem · combinatorics
Matrix.IsHadamard.conjTranspose
∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] [inst_3 : StarRing R]
{A : Matrix n n R}, A.IsHadamard → A.conjTranspose.IsHadamardThe conjugate transpose of a Hadamard matrix is Hadamard.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- StarRingstatement and proof · cited by 1,686
- Fintype.cardproof · cited by 1,386
- Matrix.conjTransposestatement and proof · cited by 202
- Matrix.conjTranspose_conjTransposeproof · cited by 31
- Matrix.IsHadamardstatement and proof · cited by 24
- Matrix.IsHadamard.mul_conjTransposeproof · cited by 9
- Matrix.IsHadamard.apply_memproof · cited by 6
- Matrix.IsHadamard.conjTranspose_mulproof · cited by 5
- Unitary.star_memproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- Matrix.isHadamard_conjTranspose_iffproof · cited by 0
- Matrix.IsHadamard.card_eq_star_mul_of_const_row_sumproof · cited by 0