`BookProof.ChapterIrreversible.entropy_bornDist_eq_zero_iff` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : entropy (bornDist v) = 0 ↔ IsDeterministicColumn v

Initializing...

`BookProof.ChapterIrreversible.entropy_bornDist_eq_zero_iff` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : entropy (bornDist v) = 0 ↔ IsDeterministicColumn v · Prove2Me