theorem
proved
channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional
show as:
channel_eq_zero_of_isAmplitudeLinear_isDensityOnly_unconditional