Structures · Algebra
RootPairing.IsReduced
A root pairing is said to be reduced if any linearly dependent pair of roots is related by a
sign.
TODO Consider redefining this to make it perfectly symmetric between roots and coroots (i.e., so
that the same demand is made of coroots) and turning RootPairing.instFlipIsReduced into a
convenience constructor.
- Defined in
- Mathlib.LinearAlgebra.RootSystem.Reduced
- Shape
- One type argument · adds eq_or_eq_neg
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed
- RootPairing.IsReduced.linearIndependent
- RootPairing.nsmul_notMem_range_root
- RootPairing.linearIndependent_of_add_mem_range_root'
- RootPairing.Base.induction_reflect
- RootPairing.EmbeddedG2.ofPairingInThree
- RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'
- RootPairing.GeckConstruction.basis
- RootPairing.linearIndependent_of_add_mem_range_root
- RootPairing.InvariantForm.apply_eq_or
- RootPairing.GeckConstruction.isNilpotent_e
- RootPairing.GeckConstruction.lie_e_f_same
- RootPairing.linearIndependent_of_sub_mem_range_root
- RootPairing.InvariantForm.apply_eq_or_aux
- RootPairing.baseOf_root_eq_baseOf_coroot
- RootPairing.InvariantForm.apply_eq_or_of_apply_ne
- RootPairing.Base.IsPos.reflectionPerm
- RootPairing.Base.IsPos.add_zsmul
- RootPairing.not_isG2_iff_isNotG2
- RootPairing.chainBotCoeff_mul_chainTopCoeff
- RootPairing.forall_pairingIn_eq_swap_or
- RootPairing.IsReduced.eq_or_eq_neg
- RootPairing.Base.mk'
- RootPairing.Base.forall_mem_support_invtSubmodule_iff
- RootPairing.coxeterWeightIn_ne_four
- RootPairing.chainBotCoeff_mul_chainTopCoeff.isNotG2
- RootPairing.forall_pairing_eq_swap_or
- RootPairing.linearIndependent_of_sub_mem_range_root'
- RootPairing.one_le_chainTopCoeff_of_root_add_mem
- RootPairing.Base.IsPos.induction_on_reflect
- RootPairing.IsG2.pairingIn_mem_zero_one_three
- RootPairing.GeckConstruction.isNilpotent_f
- RootPairing.InvariantForm.exists_apply_eq_or
- RootPairing.IsReduced.linearIndependent_iff
- RootPairing.GeckConstruction.equivRootSystem
- RootPairing.GeckConstruction.trace_toEnd_eq_zero
- RootPairing.instFlipIsReduced
- RootPairing.GeckConstruction.isSl2Triple
- RootPairing.EmbeddedG2.ofPairingInThree_long
- RootPairing.Base.equivOfCartanMatrixEq
- RootPairing.Base.induction_on_cartanMatrix
- RootPairing.GeckConstruction.instHasTrivialRadical
- RootPairing.GeckConstruction.instIsIrreducible
- RootPairing.GeckConstruction.basis.congr_simp
- RootPairing.one_le_chainBotCoeff_of_root_add_mem
- RootPairing.coroot_mem_or_neg_mem_closure_of_root
- RootPairing.EmbeddedG2.ofPairingInThree_short
- RootPairing.GeckConstruction.basis_A_eq
- RootPairing.isNotG2_iff
- RootPairing.chainBotCoeff_add_chainTopCoeff_le_three
Ancestors0
No ancestors.