Theorems · Definition · linear algebra
Matrix.replicateCol
{m : Type u_2} → {α : Type v} → (ι : Type u_6) → (m → α) → Matrix m ι αMatrix.replicateCol ι u is the matrix with all columns equal to the vector u.
To get a column matrix with exactly one column,
Matrix.replicateCol (Fin 1) u is the canonical choice.
- Defined in
- Mathlib.LinearAlgebra.Matrix.RowCol
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Matrixstatement · cited by 4,303
- Matrix.ofproof · cited by 336
Cited by42
Results whose statement or proof uses this declaration.
- Matrix.vecMulVec_eqstatement · cited by 7
- Algebra.traceMatrix_of_basis_mulVecproof · cited by 2
- Matrix.linfty_opNNNorm_mulVecproof · cited by 2
- Matrix.linfty_opNNNorm_replicateColstatement and proof · cited by 2
- Matrix.conjTranspose_mul_self_mulVec_eq_zeroproof · cited by 1
- Matrix.transpose_replicateColstatement and proof · cited by 1
- Matrix.vecMulVec_onestatement · cited by 1
- Matrix.frobenius_norm_replicateColstatement and proof · cited by 1
- Matrix.nnnorm_replicateColstatement · cited by 1
- Matrix.trace_replicateCol_mul_replicateRowstatement · cited by 1
- Matrix.replicateCol_applystatement · cited by 1
- Matrix.replicateCol_injstatement · cited by 1