Structures · Algebra
RootPairing.IsIrreducible
A root pairing is irreducible if it is non-trivial and contains no proper invariant submodules.
- Shape
- One type argument · adds nontrivial, nontrivial', eq_top_of_invtSubmodule_reflection, eq_top_of_invtSubmodule_coreflection
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by40
- RootPairing.IsIrreducible.eq_top_of_invtSubmodule_reflection
- RootPairing.EmbeddedG2.indexEquivAllRoots
- RootPairing.IsIrreducible.nontrivial
- RootPairing.GeckConstruction.basis
- RootPairing.InvariantForm.apply_eq_or
- RootPairing.InvariantForm.apply_eq_or_of_apply_ne
- RootPairing.EmbeddedG2.span_eq_top
- RootPairing.span_orbit_eq_top
- RootPairing.not_isG2_iff_isNotG2
- RootPairing.chainBotCoeff_mul_chainTopCoeff
- RootPairing.forall_pairingIn_eq_swap_or
- RootPairing.span_root_image_eq_top_of_forall_orthogonal
- RootPairing.EmbeddedG2.basis
- RootPairing.chainBotCoeff_mul_chainTopCoeff.isNotG2
- RootPairing.exists_form_eq_form_and_form_ne_zero
- RootPairing.forall_pairing_eq_swap_or
- RootPairing.IsG2.pairingIn_mem_zero_one_three
- RootPairing.EmbeddedG2.setOfPred_index_eq_univ
- RootPairing.EmbeddedG2.mem_allRoots
- RootPairing.InvariantForm.exists_apply_eq_or
- RootPairing.GeckConstruction.equivRootSystem
- RootPairing.instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible
- RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply
- RootPairing.isSimpleModule_weylGroupRootRep
- RootPairing.Base.induction_on_cartanMatrix
- RootPairing.GeckConstruction.instHasTrivialRadical
- RootPairing.GeckConstruction.instIsIrreducible
- RootPairing.GeckConstruction.basis.congr_simp
- RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe
- RootPairing.EmbeddedG2.setOf_index_eq_univ
- RootPairing.EmbeddedG2.card_index_eq_twelve
- RootPairing.instIsIrreducibleFlip
- RootPairing.GeckConstruction.basis_A_eq
- RootPairing.isNotG2_iff
- RootPairing.EmbeddedG2.instIsG2OfIsIrreducible
- RootPairing.IsIrreducible.eq_top_of_invtSubmodule_coreflection
- RootPairing.IsIrreducible.nontrivial'
- RootPairing.GeckConstruction.lie_e_f_ne
- RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'
- RootPairing.isG2_iff
Ancestors0
No ancestors.