Structures · Algebra
RootPairing.IsValuedIn
If R is an S-algebra, a root pairing over R is said to be valued in S if the pairing
between a root and coroot always belongs to S.
Of particular interest is the case S = ℤ. See RootPairing.IsCrystallographic.
- Shape
- 2 explicit arguments · adds exists_value
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by117
- RootPairing.pairingIn
- RootPairing.algebraMap_pairingIn
- RootPairing.posRootForm
- RootPairing.RootPositiveForm.posForm
- RootPairing.RootFormIn
- RootPairing.PolarizationIn
- RootPairing.RootPositiveForm.form
- RootPairing.coroot'In
- RootPairing.pairingIn_reflectionPerm_self_left
- RootPairing.RootPositiveForm.toInvariantForm
- RootPairing.coxeterWeightIn
- RootPairing.RootPositiveForm.rootLength
- RootPairing.pairingIn_same
- RootPairing.RootPositiveForm.algebraMap_posForm
- RootPairing.Base.cartanMatrixIn
- RootPairing.pairingIn_reflectionPerm_self_right
- RootPairing.algebraMap_rootFormIn
- RootPairing.restrictScalars'
- RootPairing.Base.cartanMatrixIn_apply_same
- RootPairing.pairingIn_eq_zero_iff
- RootPairing.RootPositiveForm.zero_lt_posForm_apply_root
- RootPairing.posRootForm_eq
- RootPairing.PolarizationIn_apply
- RootPairing.PolarizationIn_eq
- RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul
- RootPairing.algebraMap_coroot'In_apply
- RootPairing.RootPositiveForm.exists_pos_eq
- RootPairing.finrank_rootSpanIn
- RootPairing.exists_value
- RootPairing.algebraMap_coxeterWeightIn
- RootPairing.zero_lt_pairingIn_iff'
- RootPairing.posRootForm_posForm_pos_of_ne_zero
- RootPairing.pairingIn.congr_simp
- RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four
- RootPairing.root'In
- RootPairing.posRootForm_rootFormIn_posDef
- RootPairing.Base.algebraMap_cartanMatrixIn_apply
- RootPairing.rootFormIn_self_smul_coroot
- RootPairing.pairingIn_eq_add_of_root_eq_add
- RootPairing.zero_lt_pairingIn_iff
- RootPairing.algebraMap_posRootForm_posForm
- RootPairing.finrank_range_polarization_eq_finrank_span_coroot
- RootPairing.reflection_apply_root'
- RootPairing.RootPositiveForm.algebraMap_rootLength
- RootPairing.RootPositiveForm.zero_lt_apply_root_root_iff
- RootPairing.Base.cartanMatrixIn_def
- RootPairing.algebraMap_pairingIn'
- RootPairing.RootPositiveForm.pairingIn_mul_eq_pairingIn_mul_swap
- RootPairing.RootPositiveForm.rootLength_pos
- RootPairing.Base.cartanMatrixIn_mul_diagonal_eq
Ancestors0
No ancestors.