462def coupledOperatorInner {N : ℕ} 463 (A B : CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N) : ℂ :=
proof body
Definition body.
464 ∑ s : CoupledCoreIndex N, ∑ t : CoupledCoreIndex N, 465 star (A (coupledBasisKet s) t) * B (coupledBasisKet s) t 466 467/-- The coupled phase character has unit modulus. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.