toMatrix_orthonormalBasis_conjTranspose_mul_self

English

Specialized version of equiv_apply_basis for index i.

Русский

Специализированная версия equiv_apply_basis для индекса i.

LaTeX

$$$$ (b.equiv b' e)(b_i) = b'_{e(i)}. $$$$

Lean4

/-- A version of `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` that works for bases with
different index types. -/
@[simp]
theorem toMatrix_orthonormalBasis_conjTranspose_mul_self [Fintype ι'] (a : OrthonormalBasis ι' 𝕜 E)
    (b : OrthonormalBasis ι 𝕜 E) : (a.toBasis.toMatrix b)ᴴ * a.toBasis.toMatrix b = 1 :=
  by
  ext i j
  convert a.repr.inner_map_map (b i) (b j)
  · simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, star_def, PiLp.inner_apply, inner_apply']
    congr
  · rw [orthonormal_iff_ite.mp b.orthonormal i j, Matrix.one_apply]

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