`BookProof.TensorCore.inner_tmul_pow` (n : ℕ) (x x' : Hs.carrier) (y y' : (Hs.pow n).carrier) : (inner ℂ (x ⊗ₜ[ℂ] y : (Hs.pow (n + 1)).carrier) (x' ⊗ₜ[ℂ] y') : ℂ) = inner ℂ x x' *

Initializing...

`BookProof.TensorCore.inner_tmul_pow` (n : ℕ) (x x' : Hs.carrier) (y y' : (Hs.pow n).carrier) : (inner ℂ (x ⊗ₜ[ℂ] y : (Hs.pow (n + 1)).carrier) (x' ⊗ₜ[ℂ] y') : ℂ) = inner ℂ x x' * · Prove2Me