Channel coherent information
import Quantum_channel import State_coherent_information /-- "The coherent information of a quantum channel -/ def coh_info_of_channel [quantum_channel 𝒩A'] : ℝ := max {coh_info_of_state I⨂𝒩A' ψAA' | pure ψAA'}
import Quantum_channel import State_coherent_information /-- "The coherent information of a quantum channel -/ def coh_info_of_channel [quantum_channel 𝒩A'] : ℝ := max {coh_info_of_state I⨂𝒩A' ψAA' | pure ψAA'}