`BookProof.ChapterTimeTranslation.measOp_apply` (U : Matrix (Fin n) (Fin n) ℂ) (a : Fin n) (k l : Fin n) : measOp U a k l = U k a * (starRingEnd ℂ) (U l a)

Initializing...

`BookProof.ChapterTimeTranslation.measOp_apply` (U : Matrix (Fin n) (Fin n) ℂ) (a : Fin n) (k l : Fin n) : measOp U a k l = U k a * (starRingEnd ℂ) (U l a) · Prove2Me