IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores
IndisputableMonolith/Foundation/OperatorCore/CoupledRecognitionCores.lean · 32 lines · 14 declarations
show as:
view math explainer →
1import IndisputableMonolith.Foundation.CoupledRecognitionCores
2
3namespace IndisputableMonolith
4namespace Foundation
5namespace OperatorCore
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
32