abbrev
definition
QuquartState
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores on GitHub at line 9.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
6
7noncomputable section
8
9abbrev QuquartState := IndisputableMonolith.Foundation.CoupledRecognitionCores.QuquartState
10abbrev basisKet := IndisputableMonolith.Foundation.CoupledRecognitionCores.basisKet
11abbrev add4 := IndisputableMonolith.Foundation.CoupledRecognitionCores.add4
12abbrev ququartX := IndisputableMonolith.Foundation.CoupledRecognitionCores.ququartX
13abbrev ququartZ := IndisputableMonolith.Foundation.CoupledRecognitionCores.ququartZ
14abbrev CoupledCoreIndex := IndisputableMonolith.Foundation.CoupledRecognitionCores.CoupledCoreIndex
15abbrev CoupledCoreSpace := IndisputableMonolith.Foundation.CoupledRecognitionCores.CoupledCoreSpace
16abbrev tensorWeylMonomial {N : ℕ} :=
17 IndisputableMonolith.Foundation.CoupledRecognitionCores.tensorWeylMonomial (N := N)
18abbrev localWeylMonomial := IndisputableMonolith.Foundation.CoupledRecognitionCores.localWeylMonomial
19abbrev ququartWeyl_relation := IndisputableMonolith.Foundation.CoupledRecognitionCores.ququartWeyl_relation
20abbrev coupledCoreIndex_card := IndisputableMonolith.Foundation.CoupledRecognitionCores.coupledCoreIndex_card
21abbrev tensorWeylMonomial_zero_zero {N : ℕ} :=
22 IndisputableMonolith.Foundation.CoupledRecognitionCores.tensorWeylMonomial_zero_zero (N := N)
23abbrev localWeylFamily_card := IndisputableMonolith.Foundation.CoupledRecognitionCores.localWeylFamily_card
24abbrev tensorWeylMonomial_self_inner {N : ℕ} :=
25 IndisputableMonolith.Foundation.CoupledRecognitionCores.tensorWeylMonomial_self_inner (N := N)
26
27end
28
29end OperatorCore
30end Foundation
31end IndisputableMonolith