Mathlib Map

Theorems · Theorem · linear algebra

Matrix.conjTranspose_conjTranspose

∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : InvolutiveStar α] (M : Matrix m n α),
  M.conjTranspose.conjTranspose = M
Defined in
Mathlib.LinearAlgebra.Matrix.ConjTranspose
Cited by
31 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Quot.sound
Assumes
InvolutiveStar
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.conjTranspose_involutive · cited by 4Matrix.conjTranspose_invo…Matrix.isHermitian_conjTranspose_mul_mul · cited by 3Matrix.isHermitian_conjTr…Matrix.PosDef.mul_mul_conjTranspose_same · cited by 2PosDef.mul_mul_conjTransp…Matrix.PosSemidef.inv · cited by 2PosSemidef.invMatrix.IsHermitian.fromBlocks₁₁ · cited by 2IsHermitian.fromBlocks₁₁Matrix.isHermitian_conjTranspose_mul_self · cited by 2Matrix.isHermitian_conjTr…Matrix.IsHadamard.conjTranspose · cited by 2IsHadamard.conjTransposeMatrix.isHermitian_mul_conjTranspose_self · cited by 1Matrix.isHermitian_mul_co…Matrix.mul_conjTranspose_mul_self_eq_zero · cited by 1Matrix.mul_conjTranspose_…Matrix.posSemidef_self_mul_conjTranspose · cited by 1Matrix.posSemidef_self_mu…Matrix.mul_self_mul_conjTranspose_eq_zero · cited by 1Matrix.mul_self_mul_conjT…Matrix.IsHermitian.fromBlocks · cited by 1IsHermitian.fromBlocksMatrix.rank_conjTranspose · cited by 1Matrix.rank_conjTransposeMatrix.PosDef.inv · cited by 1PosDef.invMatrix.self_mul_conjTranspose_mul_eq_zero · cited by 1Matrix.self_mul_conjTrans…Matrix · cited by 4303MatrixMatrix.ext · cited by 540Matrix.extMatrix.conjTranspose · cited by 202Matrix.conjTransposestar_star · cited by 135star_starInvolutiveStar · cited by 52InvolutiveStarMatrix.conjTranspose_conjTran…CITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by31

Results whose statement or proof uses this declaration.