IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForcedJoint

declarations in this module (18)

• abbrev JointSubstrate L54
• def PureTensorFactorization L60
• def evalAt L66
• theorem evalAt_apply L68
• def insertSecond L74
• theorem insertSecond_apply L77
• def insertFirst L83
• theorem insertFirst_apply L86
• def extractFirst L93
• theorem extractFirst_tmul L97
• def extractSecond L104
• theorem extractSecond_tmul L108
• theorem isAmplitudeLinear_matter_of_pureTensorFactorization L117
• theorem isAmplitudeLinear_channel_of_pureTensorFactorization L135
• theorem isAmplitudeLinear_both_of_pureTensorFactorization L152
• theorem channel_eq_zero_of_density_only_of_pureTensorFactorization L173
• theorem matter_eq_zero_of_density_only_of_pureTensorFactorization L185
• theorem not_exists_pureTensorFactorization_nontrivial_matter_density_only_channel L199