module
module
IndisputableMonolith.Gravity.QuantumChannel.AmplitudeLinearForced
show as:
view Lean formalization →
used by (3)
depends on (1)
declarations in this module (8)
-
abbrev
Signal8 -
def
IsAmplitudeLinear -
def
IsPhaseEquivariant -
def
IsDensityOnly -
theorem
isPhaseEquivariant_of_isAmplitudeLinear -
theorem
eq_zero_of_isAmplitudeLinear_isDensityOnly -
theorem
not_isDensityOnly_of_isAmplitudeLinear_of_ne_zero -
theorem
not_exists_nontrivial_isAmplitudeLinear_and_isDensityOnly