Theorems · Theorem · linear algebra

Matrix.self_mul_conjTranspose_mul_eq_zero

∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {p : Type u_5}
  (A : Matrix m n R) (B : Matrix m p R), A * A.conjTranspose * B = 0 ↔ A.conjTranspose * B = 0

Defined in

Mathlib.LinearAlgebra.Matrix.DotProduct

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypePartialOrderNonUnitalRingStarRingStarOrderedRingNoZeroDivisors