det_one_add_replicateCol_mul_replicateRow

English

Let ι be a unique index type and u, v be column/row vectors. Then det(I + replicateCol(u) replicateRow(v)) = 1 + v ⬝ᵥ u.

Русский

Пусть ι имеется как уникальный индексовый тип, и u, v — столбец и строка соответствующе. Тогда det(I + replicateCol(u) replicateRow(v)) = 1 + v^T u.

LaTeX

$$$\\det\\left(I + \\mathrm{replicateCol}_{ι}(u) \\mathrm{replicateRow}_{ι}(v)\\right) = 1 + v \\cdot u$$$

Lean4

/-- A special case of the **Matrix determinant lemma** for when `A = I`. -/
theorem det_one_add_replicateCol_mul_replicateRow {ι : Type*} [Unique ι] (u v : m → α) :
    det (1 + replicateCol ι u * replicateRow ι v) = 1 + v ⬝ᵥ u := by
  rw [det_one_add_mul_comm, det_unique, Pi.add_apply, Pi.add_apply, Matrix.one_apply_eq,
    Matrix.replicateRow_mul_replicateCol_apply]

Похожие утверждения