module
module
IndisputableMonolith.Foundation.OperatorCore.ComplexStructureForcing
show as:
view Lean formalization →
depends on (1)
declarations in this module (17)
-
abbrev
Signal8 -
abbrev
nextIdx -
abbrev
shift -
abbrev
shiftIter -
abbrev
eigenvalue -
abbrev
dft8 -
abbrev
idft8 -
abbrev
inner8 -
abbrev
JcostC -
abbrev
totalModeCost -
abbrev
UnitaryEvolution -
abbrev
shift_period_8 -
abbrev
complexification_forced -
abbrev
dft8_preserves_inner -
abbrev
jcost_phase_invariant -
abbrev
mode_cost_phase_invariant -
abbrev
cost_phase_duality