Theorems · Theorem · linear algebra
Matrix.star_mulVec
∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n] [inst_2 : StarRing α]
(M : Matrix m n α) (v : n → α), star (M.mulVec v) = Matrix.vecMul (star v) M.conjTranspose- Cited by
- 4 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- StarRingstatement and proof · cited by 1,686
- Star.starstatement · cited by 1,082
- NonUnitalSemiringstatement and proof · cited by 339
- Matrix.mulVecstatement · cited by 267
- Matrix.conjTransposestatement · cited by 202
- Matrix.vecMulstatement · cited by 148
- Matrix.star_dotProduct_starproof · cited by 3
Cited by4
Results whose statement or proof uses this declaration.
- Matrix.PosDef.conjTranspose_mul_mul_sameproof · cited by 3
- Matrix.PosSemidef.conjTranspose_mul_mul_sameproof · cited by 3
- Matrix.schur_complement_eq₁₁proof · cited by 1
- Matrix.schur_complement_eq₂₂proof · cited by 0