module module

`IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.CoupledRecognitionCores module_import

declarations in this module (14)

abbrev QuquartState L9
abbrev basisKet L10
abbrev add4 L11
abbrev ququartX L12
abbrev ququartZ L13
abbrev CoupledCoreIndex L14
abbrev CoupledCoreSpace L15
abbrev tensorWeylMonomial L16
abbrev localWeylMonomial L18
abbrev ququartWeyl_relation L19
abbrev coupledCoreIndex_card L20
abbrev tensorWeylMonomial_zero_zero L21
abbrev localWeylFamily_card L23
abbrev tensorWeylMonomial_self_inner L24