invertibleLowerInv — Mathlib

English

Kronecker product of two diagonals is diagonal with entries a_i ⊗ b_j.

Русский

Кронекерово произведение двух диагоналей диагональное; элементы равны a_i ⊗ b_j.

LaTeX

$$kroneckerMap (diagonal a) (diagonal b) = diagonal (λ mn, a m ⊗ₜ b n)$$

Lean4

noncomputable instance invertibleLowerInv : Invertible (LDL.lowerInv hS) :=
  by
  rw [LDL.lowerInv_eq_gramSchmidtBasis]
  haveI :=
    Basis.invertibleToMatrix (Pi.basisFun 𝕜 n)
      (@gramSchmidtBasis 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _ (Pi.basisFun 𝕜 n))
  infer_instance

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