Structures · Algebra
RootPairing.IsRootSystem
A root system is a root pairing for which the roots and coroots span their ambient modules.
- Defined in
- Mathlib.LinearAlgebra.RootSystem.Defs
- Shape
- One type argument · adds span_root_eq_top, span_coroot_eq_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by62
- RootPairing.IsRootSystem.span_root_eq_top
- RootPairing.Base.toWeightBasis
- RootPairing.PolarizationEquiv
- RootPairing.Base.toWeightBasis_apply
- RootPairing.IsRootSystem.span_coroot_eq_top
- RootPairing.Base.toCoweightBasis
- RootPairing.linearIndepOn_root_baseOf
- RootPairing.finrank_rootSpanIn
- RootPairing.eq_baseOf_of_linearIndepOn_of_mem_or_neg_mem_closure
- RootPairing.Base.cartanMatrix_nondegenerate
- RootPairing.Base.cartanMatrixIn_mul_diagonal_eq
- RootPairing.GeckConstruction.basis
- RootPairing.eq_zero_iff_forall_coroot'_eq_zero
- RootPairing.coroot_eq_polarizationEquiv_apply_root
- RootPairing.span_root'_eq_top
- RootPairing.polarizationEquiv_apply
- RootPairing.baseOf_root_eq_baseOf_coroot
- RootPairing.rootForm_nondegenerate
- RootPairing.Base.exists_cartanMatrix_mul_diagaonal_posDef
- RootPairing.finrank_rootSpanIn_int
- RootPairing.Base.injective_pairingIn
- RootPairing.polarizationEquiv_toLinearMap
- RootPairing.Base.cartanMatrixIn_nondegenerate
- RootPairing.Base.mk'
- RootPairing.Base.cartanMatrix_mul_diagonal_eq
- RootPairing.invtRootSubmodule.eq_span_root
- RootPairing.Base.toCoweightBasis_apply
- RootPairing.ncard_eq_finrank_of_linearIndepOn_of
- RootPairing.Base.exists_cartanMatrix_diagaonal_mul_posDef
- RootPairing.GeckConstruction.equivRootSystem
- RootPairing.span_coroot'_eq_top
- RootPairing.invtRootSubmodule.eq_top_iff
- RootPairing.linearIndepOn_coroot_iff
- RootPairing.Base.equivOfCartanMatrixEq
- RootPairing.invtRootSubmodule.eq_bot_iff
- RootPairing.GeckConstruction.linearIndependent_h
- RootPairing.PolarizationEquiv.congr_simp
- RootPairing.GeckConstruction.instHasTrivialRadical
- RootPairing.GeckConstruction.instIsIrreducible
- RootPairing.GeckConstruction.basis.congr_simp
- RootPairing.reflectionPerm_eq_reflectionPerm_iff
- RootPairing.eq_baseOf_iff
- RootPairing.coroot_mem_or_neg_mem_closure_of_root
- RootPairing.finrank_corootSpanIn
- RootPairing.instIsRootSystemFlip
- RootPairing.GeckConstruction.basis_A_eq
- RootPairing.Base.toCoweightBasis_repr_coroot
- RootPairing.Equiv.mk'
- RootPairing.instIsRootSystemMap
- RootPairing.instIsBalancedOfIsRootSystem
Ancestors0
No ancestors.