theorem
proved
channel_eq_zero_of_density_only_of_pureTensorFactorization
show as:
channel_eq_zero_of_density_only_of_pureTensorFactorization