abbrev
definition
CoupledCoreIndex
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores on GitHub at line 14.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
addedConfig -
addedConfig_eq_addedConfig_iff_left -
addedConfig_shiftedConfig -
coupledBasisKet -
coupledBasisKet_orthonormal -
coupledCoreEquivFin -
CoupledCoreIndex -
coupledCoreIndex_card -
CoupledCoreSpace -
coupledOperatorInner -
embedState -
embedState_injective -
finite_dimensional_exact_embedding -
liftOperator -
liftOperator_intertwines -
phaseCharacter -
phaseCharacter_star_mul_self -
phaseCharacter_zero -
projectState -
projectState_embedState -
scaled_coupledBasisKet_inner -
shiftedConfig -
shiftedConfig_addedConfig -
shiftedConfig_zero -
tensorWeylMonomial -
tensorWeylMonomial_basis_image_orthogonal -
tensorWeylMonomial_basisKet -
tensorWeylMonomial_self_inner -
tensorWeylMonomial_shift_orthogonal
formal source
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