529def embedState {d N : ℕ} (_h : d ≤ Fintype.card (CoupledCoreIndex N)) : 530 (Fin d → ℂ) →ₗ[ℂ] CoupledCoreSpace N where 531 toFun := fun v s =>
proof body
Definition body.
532 let i := coupledCoreEquivFin N s 533 if hi : i.val < d then v ⟨i.val, hi⟩ else 0 534 map_add' := by 535 intro v w 536 ext s 537 dsimp [coupledCoreEquivFin] 538 split_ifs <;> simp 539 map_smul' := by 540 intro z v 541 ext s 542 dsimp [coupledCoreEquivFin] 543 split_ifs <;> simp 544 545/-- Restrict a coupled-core state back to the first `d` coordinates of the 546enumerated basis. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.