Base

📁 Source: Mathlib/LinearAlgebra/RootSystem/Base.lean

Statistics

Metric	Count
Definitions Base, Base, IsPos, flip, height, support, toCoweightBasis, toWeightBasis, Base	9
Theorems add, add_zsmul, exists_mem_support_pos_pairingIn, induction_on_add, induction_on_reflect, neg_iff_not, or_neg, reflectionPerm, sub, chainBotCoeff_eq_zero, chainTopCoeff_eq_of_ne, coroot_mem_or_neg_mem, coroot_mem_span_int, eq_one_or_neg_one_of_mem_support_of_smul_mem, eq_one_or_neg_one_of_mem_support_of_smul_mem_aux, exists_eq_sum_and_forall_sum_mem_of_isPos, exists_mem_support_pos_pairingIn_ne_zero, exists_root_eq_sum_int, exists_root_eq_sum_nat_or_neg, flip_support, forall_mem_support_invtSubmodule_iff, height_add, height_add_zsmul, height_eq_sum, height_ne_zero, height_one_of_mem_support, height_reflectionPerm_self, height_sub, induction_add, induction_reflect, isPos_iff, isPos_iff', isPos_of_mem_support, linearIndepOn_coroot, linearIndepOn_root, linearIndependent_pair_of_ne, not_nonneg_iff_neg_of_sum_mem_range_root, not_nonpos_iff_pos_of_sum_mem_range_root, pairingIn_le_zero_of_ne, pos_or_neg_of_sum_smul_root_mem, root_mem_or_neg_mem, root_mem_span_int, root_ne_neg_of_ne, span_coroot_support, span_int_coroot_support, span_int_root_support, span_root_support, sub_notMem_range_coroot, sub_notMem_range_root, support_nonempty, toCoweightBasis_apply, toCoweightBasis_repr_coroot, toWeightBasis_apply, toWeightBasis_repr_root	54
Total	63

FiberBundleCore

Definitions

Name	Category	Theorems
Base 📖	CompOp	—

RootPairing

Definitions

Name	Category	Theorems
Base 📖	CompData	1 math math: nonempty_base

RootPairing.Base

Definitions

Name	Category	Theorems
IsPos 📖	MathDef	5 math math: IsPos.or_neg, isPos_of_mem_support, IsPos.neg_iff_not, isPos_iff, isPos_iff'
flip 📖	CompOp	1 math math: flip_support
height 📖	CompOp	8 math math: height_reflectionPerm_self, height_eq_sum, height_add_zsmul, height_one_of_mem_support, height_sub, height_add, isPos_iff, isPos_iff'
support 📖	CompOp	76 math math: exists_mem_support_pos_pairingIn_ne_zero, RootPairing.GeckConstruction.h_def, RootPairing.GeckConstruction.isSl2Triple, span_coroot_support, cartanMatrixIn_def, algebraMap_cartanMatrixIn_apply, RootPairing.GeckConstruction.instHasTrivialRadical, injective_pairingIn, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, cartanMatrix_map_abs, root_mem_span_int, RootPairing.GeckConstruction.trace_h_eq_zero, cartanMatrixIn_nondegenerate, cartanMatrix_apply_eq_zero_iff, linearIndependent_pair_of_ne, linearIndepOn_coroot, cartanMatrix_nondegenerate, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, exists_root_eq_sum_nat_or_neg, exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, coroot_mem_span_int, RootPairing.GeckConstruction.lie_h_e, RootPairing.GeckConstruction.trace_toEnd_eq_zero, cartanMatrix_apply_eq_zero_iff_pairing, chainBotCoeff_eq_zero, RootPairing.GeckConstruction.span_range_h'_eq_top, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.span_range_h_le_range_diagonal, RootPairing.GeckConstruction.ω_mul_h, RootPairing.GeckConstruction.instIsIrreducible, linearIndepOn_root, toCoweightBasis_apply, span_int_root_support, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, toCoweightBasis_repr_coroot, RootPairing.IsG2.card_base_support_eq_two, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, RootPairing.GeckConstruction.ωConj_invFun, RootPairing.GeckConstruction.isNilpotent_f, RootPairing.GeckConstruction.lie_e_f_same, RootPairing.GeckConstruction.ω_mul_ω, RootPairing.GeckConstruction.ωConj_toFun, RootPairing.GeckConstruction.ω_mul_e, RootPairing.GeckConstruction.isNilpotent_e, exists_root_eq_sum_int, support_nonempty, RootPairing.GeckConstruction.h_mem_lieAlgebra, root_mem_or_neg_mem, toWeightBasis_apply, cartanMatrix_eq_neg_chainTopCoeff, RootPairing.GeckConstruction.lie_h_f, RootPairing.GeckConstruction.ω_mul_f, toWeightBasis_repr_root, coroot_mem_or_neg_mem, RootPairing.GeckConstruction.lie_e_lie_f_apply, IsPos.exists_mem_support_pos_pairingIn, RootPairing.GeckConstruction.f_lie_v_same, span_root_support, cartanMatrixIn_mul_diagonal_eq, RootPairing.GeckConstruction.f_mem_lieAlgebra, exists_eq_sum_and_forall_sum_mem_of_isPos, RootPairing.GeckConstruction.e_mem_lieAlgebra, RootPairing.GeckConstruction.lie_h_h, abs_cartanMatrix_apply, RootPairing.GeckConstruction.h_eq_diagonal, span_int_coroot_support, flip_support, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, RootPairing.GeckConstruction.lie_e_f_mul_ω, RootPairing.GeckConstruction.e_lie_u, RootPairing.GeckConstruction.lie_e_f_ne, chainTopCoeff_eq_of_ne
toCoweightBasis 📖	CompOp	2 math math: toCoweightBasis_apply, toCoweightBasis_repr_coroot
toWeightBasis 📖	CompOp	3 math math: toWeightBasis_apply, toWeightBasis_repr_root, cartanMatrixIn_mul_diagonal_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chainBotCoeff_eq_zero 📖	mathematical	—	RootPairing.chainBotCoeff Finset SetLike.instMembership Finset.instSetLike support	—	RootPairing.chainBotCoeff_eq_zero_iff sub_notMem_range_root
chainTopCoeff_eq_of_ne 📖	mathematical	—	RootPairing.chainTopCoeff Finset SetLike.instMembership Finset.instSetLike support RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	RootPairing.chainTopCoeff_sub_chainBotCoeff linearIndependent_pair_of_ne chainBotCoeff_eq_zero CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero sub_zero
coroot_mem_or_neg_mem 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot SetLike.coe Finset Finset.instSetLike support NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coroot_mem_span_int 📖	mathematical	—	Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot SetLike.coe Finset Finset.instSetLike support	—	root_mem_span_int
eq_one_or_neg_one_of_mem_support_of_smul_mem 📖	mathematical	Finset Finset.instMembership support Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	eq_one_or_neg_one_of_mem_support_of_smul_mem_aux RootPairing.coroot_eq_smul_coroot_iff smul_smul one_smul Set.mem_range_self mul_comm one_mul mul_one Int.mul_eq_one_iff_eq_one_or_neg_one Nat.cast_one Int.cast_one Int.cast_neg neg_mul
eq_one_or_neg_one_of_mem_support_of_smul_mem_aux 📖	mathematical	Finset Finset.instMembership support Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	coroot_mem_span_int Finset.sum_congr SemigroupAction.mul_smul Int.cast_smul_eq_zsmul RootPairing.coroot_eq_smul_coroot_iff Submodule.mem_span_range_iff_exists_fun Set.image_eq_range RingHomInvPair.ids Subtype.finite map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Finite.of_fintype Finsupp.linearCombination_eq_fintype_linearCombination_apply Fintype.linearCombination_apply Finsupp.linearCombination_single one_smul linearIndepOn_coroot mul_comm Finsupp.single_eq_same DFunLike.congr_fun
exists_eq_sum_and_forall_sum_mem_of_isPos 📖	mathematical	IsPos	Set Set.instHasSubset Set.range SetLike.coe Finset Finset.instSetLike support DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid Finset.univ Fin.fintype Set.instMembership Finset.Iic PartialOrder.toPreorder Fin.instPartialOrder Fin.instLocallyFiniteOrderBot	—	IsPos.induction_on_add Matrix.range_cons Matrix.range_empty Set.union_empty Finset.sum_congr Finset.univ_unique Matrix.cons_val_fin_one Finset.sum_const Finset.card_singleton one_smul Fin.card_Iic zero_add Function.instEmbeddingLikeEmbedding Fin.range_snoc Set.insert_subset Fin.sum_univ_castSucc Fin.snoc_castSucc Fin.snoc_last Fin.sum_Iic_castSucc Finset.ext
exists_mem_support_pos_pairingIn_ne_zero 📖	mathematical	—	Finset Finset.instMembership support	—	IsPos.or_neg IsPos.exists_mem_support_pos_pairingIn LT.lt.ne' RootPairing.pairingIn_reflectionPerm_self_right instFaithfulSMulIntOfCharZero
exists_root_eq_sum_int 📖	mathematical	—	Set Set.instHasSubset Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing SetLike.coe Finset Finset.instSetLike support Preorder.toLT Pi.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder Pi.instZero DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	exists_root_eq_sum_nat_or_neg Pi.lt_def IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing RootPairing.ne_zero CharZero.NeZero.two Finset.sum_congr zero_nsmul Finset.sum_const_zero natCast_zsmul Function.support_neg Int.instAddLeftMono neg_zero neg_smul Finset.sum_neg_distrib
exists_root_eq_sum_nat_or_neg 📖	mathematical	—	Set Set.instHasSubset Function.support MulZeroClass.toZero Nat.instMulZeroClass SetLike.coe Finset Finset.instSetLike support DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddSubmonoid.closure_induction Pi.support_single_of_ne Finset.sum_congr Pi.single_apply ite_smul one_smul zero_nsmul Finset.sum_ite_eq' Function.support_zero Finset.sum_const_zero HasSubset.Subset.trans Set.instIsTransSubset Function.support_add Set.union_subset_iff add_smul Finset.sum_add_distrib root_mem_or_neg_mem
flip_support 📖	mathematical	—	support RootPairing.flip flip	—	—
forall_mem_support_invtSubmodule_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Module.End.invtSubmodule LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RootPairing.reflection	—	RingHomInvPair.ids LinearEquiv.ext RootPairing.coroot_reflectionPerm RootPairing.coreflection_apply_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass RootPairing.root_reflectionPerm Nat.instAtLeastTwoHAddOfNat RootPairing.pairing_same two_smul sub_add_cancel_right smul_neg neg_smul neg_neg induction_reflect RootPairing.reflection_reflectionPerm Module.End.invtSubmodule.comp
height_add 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	height	—	exists_root_eq_sum_int Finset.sum_congr add_smul Finset.sum_add_distrib height_eq_sum
height_add_zsmul 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	height Int.instAddGroup	—	exists_root_eq_sum_int Finset.sum_congr add_smul smul_assoc AddCommGroup.intIsScalarTower Finset.sum_add_distrib height_eq_sum Finset.smul_sum
height_eq_sum 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid support SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	height Int.instAddCommMonoid	—	exists_root_eq_sum_int Fintype.linearIndependent_iffₛ LinearIndependent.restrict_scalars' AddCommGroup.intIsScalarTower instFaithfulSMulIntOfCharZero IsScalarTower.right linearIndepOn_root Finset.sum_congr Finset.sum_subtype
height_ne_zero 📖	—	—	—	—	exists_root_eq_sum_int height_eq_sum LT.lt.ne' Finset.sum_pos' IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing LT.lt.le le_antisymm Mathlib.Tactic.Push.not_and_eq RootPairing.ne_zero CharZero.NeZero.two Finset.sum_congr zero_smul Finset.sum_const_zero LT.lt.ne Finset.sum_neg'
height_one_of_mem_support 📖	mathematical	Finset Finset.instMembership support	height	—	Finset.sum_eq_single_of_mem Pi.single_eq_of_ne zero_smul Pi.single_eq_same one_smul height_eq_sum Finset.sum_pi_single'
height_reflectionPerm_self 📖	mathematical	—	height InvolutiveNeg.toNeg RootPairing.indexNeg	—	exists_root_eq_sum_int RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self Finset.sum_congr neg_smul Finset.sum_neg_distrib height_eq_sum
height_sub 📖	mathematical	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	height	—	RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.reflection_apply_self sub_eq_add_neg height_reflectionPerm_self height_add
induction_add 📖	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	—	IsPos.or_neg IsPos.induction_on_add neg_neg
induction_reflect 📖	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	—	IsPos.or_neg IsPos.induction_on_reflect neg_neg
isPos_iff 📖	mathematical	—	IsPos height	—	—
isPos_iff' 📖	mathematical	—	IsPos height	—	isPos_iff height_ne_zero
isPos_of_mem_support 📖	mathematical	Finset Finset.instMembership support	IsPos	—	isPos_iff height_one_of_mem_support
linearIndepOn_coroot 📖	mathematical	—	LinearIndepOn DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe Finset Finset.instSetLike support	—	—
linearIndepOn_root 📖	mathematical	—	LinearIndepOn DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe Finset Finset.instSetLike support	—	—
linearIndependent_pair_of_ne 📖	mathematical	—	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset SetLike.instMembership Finset.instSetLike support Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	linearIndepOn_id_range_iff Function.instEmbeddingLikeEmbedding Matrix.range_cons Matrix.range_empty Set.union_empty Set.union_singleton Set.image_pair LinearIndepOn.id_image LinearIndepOn.mono linearIndepOn_root
not_nonneg_iff_neg_of_sum_mem_range_root 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid support SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.instHasSubset Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing SetLike.coe Finset Finset.instSetLike	Pi.hasLe Pi.instZero Preorder.toLT Pi.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder	—	RootPairing.neg_mem_range_root_iff Finset.sum_congr neg_smul Finset.sum_neg_distrib neg_neg not_nonpos_iff_pos_of_sum_mem_range_root Function.support_neg IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid Int.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Pi.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd
not_nonpos_iff_pos_of_sum_mem_range_root 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid support SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.instHasSubset Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing SetLike.coe Finset Finset.instSetLike	Pi.hasLe Pi.instZero Preorder.toLT Pi.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder	—	Pi.lt_def pos_or_neg_of_sum_smul_root_mem le_of_lt Mathlib.Tactic.Contrapose.contrapose₂ le_antisymm
pairingIn_le_zero_of_ne 📖	mathematical	Finset Finset.instMembership support	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	sub_notMem_range_root RootPairing.root_sub_root_mem_of_pairingIn_pos
pos_or_neg_of_sum_smul_root_mem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finset.sum AddCommGroup.toAddCommMonoid support SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.instHasSubset Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing SetLike.coe Finset Finset.instSetLike	Preorder.toLT Pi.preorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder Pi.instZero	—	Finset.sum_finset_coe Fintype.mem_span_image_iff_exists_fun Submodule.mem_toAddSubmonoid Submodule.span_nat_eq_addSubmonoidClosure Fintype.linearIndependent_iffₛ LinearIndependent.restrict_scalars' AddCommGroup.intIsScalarTower instFaithfulSMulIntOfCharZero IsScalarTower.right linearIndepOn_root Finset.sum_congr natCast_zsmul IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Mathlib.Tactic.Contrapose.contrapose₄ Pi.lt_def le_antisymm RootPairing.ne_zero CharZero.NeZero.two zero_smul Finset.sum_const_zero root_mem_or_neg_mem IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Pi.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Pi.isOrderedAddMonoid Int.instIsOrderedAddMonoid neg_smul Finset.sum_neg_distrib Function.support_neg
root_mem_or_neg_mem 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SetLike.coe Finset Finset.instSetLike support NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
root_mem_span_int 📖	mathematical	—	Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SetLike.coe Finset Finset.instSetLike support	—	root_mem_or_neg_mem Submodule.span_span_of_tower AddCommMonoid.nat_isScalarTower Submodule.subset_span neg_mem_iff AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass
root_ne_neg_of_ne 📖	—	Finset Finset.instMembership support	—	—	linearIndepOn_iff' linearIndepOn_root Finset.coe_insert Finset.coe_singleton Finset.sum_congr one_smul Finset.sum_pair neg_add_cancel NeZero.one
span_coroot_support 📖	mathematical	—	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot SetLike.coe Finset Finset.instSetLike support RootPairing.corootSpan	—	span_root_support
span_int_coroot_support 📖	mathematical	—	Submodule.span Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot SetLike.coe Finset Finset.instSetLike support Set.range	—	span_int_root_support
span_int_root_support 📖	mathematical	—	Submodule.span Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SetLike.coe Finset Finset.instSetLike support Set.range	—	le_antisymm Submodule.span_mono Set.image_subset_range Submodule.span_le root_mem_span_int
span_root_support 📖	mathematical	—	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SetLike.coe Finset Finset.instSetLike support RootPairing.rootSpan	—	Submodule.span_span_of_tower AddCommGroup.intIsScalarTower span_int_root_support
sub_notMem_range_coroot 📖	mathematical	Finset Finset.instMembership support	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_notMem_range_root
sub_notMem_range_root 📖	mathematical	Finset Finset.instMembership support	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	eq_or_ne sub_self RootPairing.ne_zero CharZero.NeZero.two Finset.sum_subset zero_smul Finset.sum_insert Finset.sum_singleton one_smul neg_smul sub_eq_add_neg pos_or_neg_of_sum_smul_root_mem Finset.sum_congr ite_smul le_of_lt
support_nonempty 📖	mathematical	—	Finset.Nonempty support	—	Nat.instAtLeastTwoHAddOfNat Finset.coe_empty Set.image_empty AddSubmonoid.closure_empty RootPairing.ne_zero root_mem_or_neg_mem
toCoweightBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Finset SetLike.instMembership Finset.instSetLike support CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Basis.instFunLike toCoweightBasis Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot	—	toWeightBasis_apply RootPairing.instIsRootSystemFlip
toCoweightBasis_repr_coroot 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp Finset SetLike.instMembership Finset.instSetLike support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr toCoweightBasis Function.Embedding Function.instFunLikeEmbedding RootPairing.coroot Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids Module.Basis.repr_symm_apply Finsupp.linearCombination_single toCoweightBasis_apply one_smul
toWeightBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Finset SetLike.instMembership Finset.instSetLike support CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Basis.instFunLike toWeightBasis Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	linearIndepOn_root
toWeightBasis_repr_root 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp Finset SetLike.instMembership Finset.instSetLike support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr toWeightBasis Function.Embedding Function.instFunLikeEmbedding RootPairing.root Finsupp.single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids Module.Basis.repr_symm_apply Finsupp.linearCombination_single toWeightBasis_apply one_smul

RootPairing.Base.IsPos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	—	RootPairing.Base.IsPos DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—	RootPairing.Base.isPos_iff RootPairing.Base.height_add
add_zsmul 📖	—	RootPairing.Base.IsPos Finset Finset.instMembership RootPairing.Base.support DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—	RootPairing.IsReduced.linearIndependent neg_eq_iff_eq_neg RootPairing.Base.height_one_of_mem_support RootPairing.Base.height_reflectionPerm_self RootPairing.Base.isPos_iff Int.induction_on congr_simp zero_smul add_zero Function.instEmbeddingLikeEmbedding Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_mul Nat.cast_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add natCast_zsmul RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff Mathlib.Tactic.Module.NF.add_eq_eval₂ add RootPairing.Base.isPos_of_mem_support Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.mul_one neg_smul sub_eq_add_neg RootPairing.root_sub_nsmul_mem_range_iff_le_chainBotCoeff Mathlib.Tactic.Module.NF.sub_eq_eval₂ sub
exists_mem_support_pos_pairingIn 📖	mathematical	RootPairing.Base.IsPos	Finset Finset.instMembership RootPairing.Base.support RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	RootPairing.Base.exists_root_eq_sum_int Mathlib.Tactic.Contrapose.contrapose₃ Finset.sum_nonpos Int.instAddLeftMono LT.lt.le RootPairing.Base.height_eq_sum RootPairing.Base.isPos_iff FaithfulSMul.algebraMap_injective instFaithfulSMulIntOfCharZero RootPairing.algebraMap_pairingIn map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Algebra.to_smulCommClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finset.sum_congr map_zsmul LinearMap.coe_sum Finset.sum_apply zsmul_eq_mul smul_nonpos_of_nonneg_of_nonpos IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Int.instIsStrictOrderedRing Mathlib.Tactic.Push.not_and_eq MulZeroClass.zero_mul Nat.instAtLeastTwoHAddOfNat RootPairing.pairingIn_same
induction_on_add 📖	—	RootPairing.Base.IsPos	—	—	Int.induction_on RootPairing.Base.height_ne_zero exists_mem_support_pos_pairingIn eq_or_ne RootPairing.zero_lt_pairingIn_iff' Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower RootPairing.root_sub_root_mem_of_pairingIn_pos RootPairing.Base.height_sub RootPairing.Base.height_one_of_mem_support RootPairing.Base.isPos_iff' Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Module.NF.eq_const_cons Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add RootPairing.Base.isPos_iff
induction_on_reflect 📖	—	RootPairing.Base.IsPos DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	—	exists_mem_support_pos_pairingIn eq_or_ne RootPairing.zero_lt_pairingIn_iff' Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower reflectionPerm RingHomInvPair.ids RootPairing.reflection_apply_root' RootPairing.Base.height_add_zsmul neg_smul sub_eq_add_neg RootPairing.root_reflectionPerm RootPairing.Base.isPos_iff RootPairing.Base.isPos_of_mem_support neg_mul IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono contravariant_lt_of_covariant_le IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE RootPairing.Base.isPos_iff' RootPairing.reflectionPerm_self
neg_iff_not 📖	mathematical	—	RootPairing.Base.IsPos InvolutiveNeg.toNeg RootPairing.indexNeg	—	RootPairing.Base.isPos_iff RootPairing.Base.height_reflectionPerm_self RootPairing.Base.height_ne_zero
or_neg 📖	mathematical	—	RootPairing.Base.IsPos InvolutiveNeg.toNeg RootPairing.indexNeg	—	RootPairing.Base.isPos_iff RootPairing.Base.height_reflectionPerm_self RootPairing.Base.height_ne_zero
reflectionPerm 📖	mathematical	RootPairing.Base.IsPos Finset Finset.instMembership RootPairing.Base.support	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	RingHomInvPair.ids RootPairing.root_reflectionPerm neg_smul RootPairing.reflection_apply_root' AddCommGroup.intIsScalarTower sub_eq_add_neg add_zsmul
sub 📖	—	RootPairing.Base.IsPos Finset Finset.instMembership RootPairing.Base.support DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—	RootPairing.Base.isPos_iff' RootPairing.Base.height_sub RootPairing.Base.height_one_of_mem_support RootPairing.Base.isPos_iff

VectorBundleCore

Definitions

Name	Category	Theorems
Base 📖	CompOp	—

---

← Back to Index