`BookProof.TensorCore.derPow_symm` (hA : SymmetricOn D₂ A) (n : ℕ) : ∀ x y : ((domSpace Hs D₂).pow n), (inner ℂ (derPow Hs D₂ A n x) (inclPow Hs D₂ n y) : ℂ) = inner ℂ (inclPow Hs

Initializing...

`BookProof.TensorCore.derPow_symm` (hA : SymmetricOn D₂ A) (n : ℕ) : ∀ x y : ((domSpace Hs D₂).pow n), (inner ℂ (derPow Hs D₂ A n x) (inclPow Hs D₂ n y) : ℂ) = inner ℂ (inclPow Hs · Prove2Me