| Name | Category | Theorems |
|---|
IsOrthogonal 📖 | MathDef | 4 mathmath: EmbeddedG2.isOrthogonal_short_and_long, coxeterWeight_zero_iff_isOrthogonal, isOrthogonal_symm, isOrthogonal_iff_pairing_eq_zero
|
IsRootSystem 📖 | CompData | 6 mathmath: instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', instIsRootSystemMap, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible, instIsRootSystemFlip, isRootSystem_mk''
|
coreflection 📖 | CompOp | 20 mathmath: coreflection_eq_flip_reflection, coreflection_image_eq, range_weylGroup_coweightHom, IsOrthogonal.coreflection_apply_right, coreflection_inv, corootSpan_mem_invtSubmodule_coreflection, coreflection_apply_self, bijOn_coreflection_coroot, reflection_dualMap_eq_coreflection, coreflection_sq, coreflection_apply, coroot_eq_coreflection_of_root_eq, toPerfPair_conj_reflection, toPerfPair_flip_conj_coreflection, coreflection_same, IsOrthogonal.coreflection_apply_left, coroot_reflectionPerm, coreflection_apply_coroot, mapsTo_coreflection_coroot, Equiv.reflection_coweightEquiv
|
coroot 📖 | CompOp | 60 mathmath: rootForm_self_smul_coroot, four_nsmul_coPolarization_compl_polarization_apply_root, Polarization_apply, coroot_eq_polarizationEquiv_apply_root, instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', Base.span_coroot_support, root_coroot_two, restrictScalars_coe_coroot, Base.sub_notMem_range_coroot, coreflection_image_eq, LieAlgebra.IsKilling.rootSystem_coroot_apply, root_coroot_eq_pairing, Base.linearIndepOn_coroot, coroot_eq_smul_coroot_iff, root'_coroot_eq_pairing, injOn_dualMap_subtype_span_root_coroot, restrictScalars_pairing, zero_notMem_range_coroot, Base.coroot_mem_span_int, IsOrthogonal.coreflection_apply_right, neg_mem_range_coroot_iff, coroot_mem_or_neg_mem_closure_of_root, reflectionPerm_coroot, smul_coroot_eq_of_root_add_root_eq, prod_rootForm_smul_coroot_mem_range_domRestrict, Hom.coroot_coweightMap, toPerfPair_flip_comp_coroot, reflectionPerm_root, flip_root, coreflection_apply_self, bijOn_coreflection_coroot, coroot_eq_neg_iff, Base.toCoweightBasis_apply, PolarizationIn_apply, Base.toCoweightBasis_repr_coroot, coroot_root_two, prod_rootFormIn_smul_coroot_mem_range_PolarizationIn, restrictScalars_coe_root, coroot_root_eq_pairing, polarizationEquiv_symm_apply_coroot, linearIndepOn_coroot_iff, coreflection_apply, coroot_eq_coreflection_of_root_eq, ext_iff, rootFormIn_self_smul_coroot, corootForm_self_smul_root, neg_coroot_mem, Base.coroot_mem_or_neg_mem, pairing_smul_coroot_eq, restrictScalars_toLinearMap_apply_apply, Hom.coroot_coweightMap_apply, IsOrthogonal.coreflection_apply_left, smul_coroot_eq_of_root_eq_smul, IsRootSystem.span_coroot_eq_top, Base.span_int_coroot_support, coroot_reflectionPerm, coreflection_apply_coroot, mapsTo_coreflection_coroot, flip_coroot, reflectionPerm_eq_iff_smul_coroot
|
coroot' 📖 | CompOp | 15 mathmath: Polarization_apply, span_coroot'_eq_top, exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, corootSpan_map_flip_toPerfPair, coroot'_apply_apply_mem_of_mem_span, corootSpan_dualAnnihilator_map_eq, toPerfPair_flip_comp_coroot, rootForm_apply_apply, iInf_ker_coroot'_eq, algebraMap_coroot'In_apply, coroot'_reflection, reflection_apply, corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', root_coroot'_eq_pairing, coroot'_reflectionPerm
|
coxeterWeight 📖 | CompOp | 6 mathmath: coxeterWeight_flip, algebraMap_coxeterWeightIn, coxeterWeight_zero_iff_isOrthogonal, coxeterWeight_swap, coxeterWeight_eq_four_iff_not_linearIndependent, four_smul_rootForm_sq_eq_coxeterWeight_smul
|
flip 📖 | CompOp | 26 mathmath: coreflection_eq_flip_reflection, rootSpan_dualAnnihilator_le_ker_rootForm, IsOrthogonal.flip, Hom.weight_coweight_transpose, coxeterWeight_flip, flip_comp_polarization_eq_rootForm, flipEquiv_apply, instIsValuedInFlip, flipEquiv_symm_apply, flip_root, Hom.weight_coweight_transpose_apply, CoPolarization_eq, flip_reflectionPerm, instIsIrreducibleFlip, flip_toFun_apply, rootSpan_dualAnnihilator_map_eq_iInf_ker_root', flip_flip, flip_toLinearMap, instIsRootSystemFlip, rootSpan_dualAnnihilator_map_eq, pairing_flip, Base.flip_support, instIsAnisotropicFlip, ker_corootForm_eq_dualAnnihilator, instFlipIsReduced, flip_coroot
|
flipEquiv 📖 | CompOp | 2 mathmath: flipEquiv_apply, flipEquiv_symm_apply
|
indexNeg 📖 | CompOp | 5 mathmath: Base.height_reflectionPerm_self, Base.IsPos.or_neg, Base.IsPos.neg_iff_not, indexNeg_neg, EmbeddedG2.setOf_index_eq_univ
|
map 📖 | CompOp | 1 mathmath: instIsRootSystemMap
|
pairing 📖 | CompOp | 47 mathmath: pairing_two_two_iff, pairing_smul_root_eq_of_not_linearIndependent, Base.algebraMap_cartanMatrixIn_apply, reflectionPerm_eq_iff_smul_root, InvariantForm.pairing_mul_eq_pairing_mul_swap, root_coroot_eq_pairing, root'_coroot_eq_pairing, restrictScalars_pairing, pairing_eq_zero_iff, pairing_eq_zero_iff', pairing_one_four_iff', pairing_reflectionPerm_self_left, pairing_reflectionPerm_self_right, exists_value, pairing_eq_add_of_root_eq_add, rootForm_root_self, smul_coroot_eq_of_root_add_root_eq, Base.cartanMatrix_apply_eq_zero_iff_pairing, pairing_neg_one_neg_four_iff, algebraMap_pairingIn, pairing_eq_zero_of_add_notMem_of_sub_notMem, isValuedIn_iff_mem_range, isValuedIn_iff, pairing_same, EmbeddedG2.pairing_long_short, RootPositiveForm.two_mul_apply_root_root, coroot_root_eq_pairing, IsValuedIn.exists_value, LieAlgebra.IsKilling.rootSystem_pairing_apply, pairing_neg_one_neg_four_iff', EmbeddedG2.pairing_short_long, InvariantForm.apply_root_root_zero_iff, pairing_smul_coroot_eq, pairing_smul_root_eq, pairing_eq_add_of_root_eq_smul_add_smul, pairing_one_four_iff, pairing_flip, pairing_reflectionPerm, isFixedPt_reflectionPerm_iff, root_coroot'_eq_pairing, InvariantForm.two_mul_apply_root_root, coreflection_apply_coroot, forall_pairing_eq_swap_or, isOrthogonal_iff_pairing_eq_zero, reflection_apply_root, reflectionPerm_eq_iff_smul_coroot, pairing_neg_two_neg_two_iff
|
reflection 📖 | CompOp | 38 mathmath: InvariantForm.apply_reflection_reflection, coreflection_eq_flip_reflection, two_nsmul_reflection_eq_of_perm_eq, Base.forall_mem_support_invtSubmodule_iff, mapsTo_reflection_root, reflection_apply_root', RootSystem.reflectionPerm_eq_reflectionPerm_iff, IsOrthogonal.reflection_apply_left, mem_invtRootSubmodule_iff, reflection_same, reflection_sq, RootPositiveForm.isOrthogonal_reflection, InvariantForm.isOrthogonal_reflection, reflectionPerm_eq_reflectionPerm_iff_of_isSMulRegular, bijOn_reflection_root, rootForm_reflection_reflection_apply, IsOrthogonal.reflection_apply_right, reflectionPerm_eq_reflectionPerm_iff_of_span, reflection_dualMap_eq_coreflection, reflection_apply_self, isFixedPt_reflection_of_isOrthogonal, coroot'_reflection, toPerfPair_conj_reflection, reflection_inv, rootSpan_mem_invtSubmodule_reflection, toPerfPair_flip_conj_coreflection, Equiv.reflection_smul, reflectionPerm_eq_reflectionPerm_iff, range_weylGroup_weightHom, reflection_apply, invtSubmodule_reflection_of_invtSubmodule_coreflection, coroot'_reflectionPerm, isOrthogonal_comm, reflection_reflectionPerm, Equiv.reflection_weightEquiv, root_reflectionPerm, reflection_image_eq, reflection_apply_root
|
reflectionPerm 📖 | CompOp | 42 mathmath: reflectionPerm_symm, chainTopCoeff_reflectionPerm_right, reflectionPerm_eq_iff_smul_root, reflectionPerm_involutive, reflectionPerm_sq, reflectionPerm_self, RootSystem.reflectionPerm_eq_reflectionPerm_iff, pairing_reflectionPerm_self_left, pairing_reflectionPerm_self_right, chainBotCoeff_reflectionPerm_right, reflectionPerm_coroot, corootSpanMem_reflectionPerm_self, reflectionPerm_eq_reflectionPerm_iff_of_isSMulRegular, pairingIn_reflectionPerm_self_left, reflectionPerm_root, coroot_eq_neg_iff, root_eq_neg_iff, pairingIn_reflectionPerm_self_right, reflectionPerm_eq_reflectionPerm_iff_of_span, RootPositiveForm.rootLength_reflectionPerm_self, chainTopCoeff_reflectionPerm_left, range_weylGroupToPerm, flip_reflectionPerm, rootSpanMem_reflectionPerm_self, pairingIn_reflectionPerm, coroot'_reflection, Equiv.reflection_indexEquiv, reflectionPerm_eq_reflectionPerm_iff, reflectionPerm_inv, reflectionPerm_eq_of_pairing_eq_zero', reflectionPerm_eq_of_pairing_eq_zero, indexNeg_neg, chainBotCoeff_reflectionPerm_left, Base.IsPos.reflectionPerm, pairing_reflectionPerm, EmbeddedG2.ofPairingInThree_long, coroot_reflectionPerm, isFixedPt_reflectionPerm_iff, coroot'_reflectionPerm, reflection_reflectionPerm, root_reflectionPerm, reflectionPerm_eq_iff_smul_coroot
|
root 📖 | CompOp | 123 mathmath: rootForm_self_smul_coroot, RootPositiveForm.algebraMap_rootLength, posRootForm_posForm_apply_apply, four_nsmul_coPolarization_compl_polarization_apply_root, linearIndepOn_root_baseOf', coroot_eq_polarizationEquiv_apply_root, instIsRootSystemSubtypeMemSubmoduleSpanRangeCoeEmbeddingRootCorootRestrictScalars', reflectionPerm_eq_iff_smul_root, Hom.root_weightMap, root_coroot_two, restrictScalars_coe_coroot, Base.root_mem_span_int, zero_notMem_range_root, InvariantForm.pairing_mul_eq_pairing_mul_swap, root_sub_root_mem_of_pairingIn_pos, span_orbit_eq_top, Hom.root_weightMap_apply, invtRootSubmodule.eq_top_iff, coxeterWeightIn_eq_four_iff_not_linearIndependent, Base.cartanMatrix_apply_eq_zero_iff, root_coroot_eq_pairing, RootPositiveForm.zero_lt_posForm_iff, Base.linearIndependent_pair_of_ne, coroot_eq_smul_coroot_iff, toPerfPair_comp_root, mapsTo_reflection_root, injOn_dualMap_subtype_span_root_coroot, restrictScalars_pairing, Base.exists_root_eq_sum_nat_or_neg, reflection_apply_root', IsOrthogonal.reflection_apply_left, pairing_one_four_iff', IsReduced.linearIndependent_iff, exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule, linearIndependent_iff_coxeterWeightIn_ne_four, weylGroup_apply_root, Equiv.root_indexEquiv_eq_smul, RootPositiveForm.exists_eq, rootForm_root_self, EmbeddedG2.indexEquivAllRoots_symm_apply, root_add_root_mem_of_pairingIn_neg, InvariantForm.exists_apply_eq_or, reflectionPerm_coroot, pairing_neg_one_neg_four_iff, bijOn_reflection_root, chainTopCoeff_eq_zero_iff, posRootForm_posForm_pos_of_ne_zero, isReduced_iff', prod_rootForm_smul_coroot_mem_range_domRestrict, IsG2.span_eq_rootSpan_int, reflectionPerm_root, flip_root, invtRootSubmodule.eq_bot_iff, linearIndepOn_root_baseOf, linearIndependent_iff_coxeterWeight_ne_four, IsRootSystem.span_root_eq_top, zero_le_posForm, IsReduced.linearIndependent, root_eq_neg_iff, Base.linearIndepOn_root, IsOrthogonal.reflection_apply_right, Base.span_int_root_support, coroot_root_two, CoPolarization_apply, RootPositiveForm.two_mul_apply_root_root, algebraMap_posRootForm_posForm, restrictScalars_coe_root, reflection_apply_self, InvariantForm.apply_eq_or_aux, pairingIn_one_four_iff, pairingIn_neg_one_neg_four_iff, neg_root_mem, RootPositiveForm.isSymm_posForm, coroot_root_eq_pairing, polarizationEquiv_symm_apply_coroot, Base.exists_root_eq_sum_int, linearIndepOn_coroot_iff, Base.root_mem_or_neg_mem, Base.toWeightBasis_apply, RootPositiveForm.exists_pos_eq, EmbeddedG2.indexEquivAllRoots_apply_coe, pairing_neg_one_neg_four_iff', posRootForm_posForm_nondegenerate, coxeterWeight_eq_four_iff_not_linearIndependent, ext_iff, corootForm_self_smul_root, exists_form_eq_form_and_form_ne_zero, Base.toWeightBasis_repr_root, InvariantForm.apply_root_root_zero_iff, RootPositiveForm.algebraMap_apply_eq_form_iff, restrictScalars_toLinearMap_apply_apply, pairing_smul_root_eq, InvariantForm.apply_eq_or, Base.span_root_support, pairingIn_neg_two_neg_two_iff, posRootForm_posForm_anisotropic, span_root_image_eq_top_of_forall_orthogonal, four_smul_rootForm_sq_eq_coxeterWeight_smul, Base.sub_notMem_range_root, neg_mem_range_root_iff, Base.cartanMatrixIn_mul_diagonal_eq, chainBotCoeff_eq_zero_iff, pairing_one_four_iff, nsmul_notMem_range_root, Base.exists_eq_sum_and_forall_sum_mem_of_isPos, RootPositiveForm.algebraMap_posForm, EmbeddedG2.allRoots_subset_range_root, reflection_apply, root_chainTopIdx, CoPolarizationIn_apply, root_coroot'_eq_pairing, InvariantForm.apply_eq_or_of_apply_ne, InvariantForm.two_mul_apply_root_root, isReduced_iff, root_chainBotIdx, LieAlgebra.IsKilling.rootSystem_root_apply, root_reflectionPerm, flip_coroot, EmbeddedG2.mem_allRoots, reflection_image_eq, baseOf_pairwise_pairing_le_zero, reflection_apply_root, pairing_neg_two_neg_two_iff
|
root' 📖 | CompOp | 12 mathmath: toPerfPair_comp_root, root'_coroot_eq_pairing, rootSpan_map_toPerfPair, corootForm_apply_apply, iInf_ker_root'_eq, CoPolarization_apply, span_root'_eq_top, root'_apply_apply_mem_of_mem_span, coreflection_apply, rootSpan_dualAnnihilator_map_eq_iInf_ker_root', rootSpan_dualAnnihilator_map_eq, algebraMap_root'In_apply
|
toLinearMap 📖 | CompOp | 38 mathmath: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, root_coroot_two, rootSpan_dualAnnihilator_le_ker_rootForm, root_coroot_eq_pairing, self_comp_coPolarization_eq_corootForm, toLinearMap_apply_CoPolarization, Hom.weight_coweight_transpose, toPerfPair_comp_root, injOn_dualMap_subtype_span_root_coroot, flip_comp_polarization_eq_rootForm, toLinearMap_apply_apply_Polarization, isPerfPair_toLinearMap, corootSpan_map_flip_toPerfPair, reflectionPerm_coroot, toLinearMap_apply_PolarizationIn, rootSpan_map_toPerfPair, IsBalanced.isPerfectCompl, corootSpan_dualAnnihilator_map_eq, toPerfPair_flip_comp_coroot, reflectionPerm_root, coroot_root_two, Hom.weight_coweight_transpose_apply, reflection_dualMap_eq_coreflection, ker_rootForm_eq_dualAnnihilator, coroot_root_eq_pairing, flip_toFun_apply, rootSpan_dualAnnihilator_map_eq_iInf_ker_root', ext_iff, toPerfPair_conj_reflection, flip_toLinearMap, restrictScalars_toLinearMap_apply_apply, toPerfPair_flip_conj_coreflection, corootSpan_dualAnnihilator_le_ker_rootForm, rootSpan_dualAnnihilator_map_eq, toLinearMap_apply_apply_mem_range_algebraMap, corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', invtSubmodule_reflection_of_invtSubmodule_coreflection, ker_corootForm_eq_dualAnnihilator
|