Chain

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

Statistics

Metric	Count
Definitions chainBotCoeff, chainBotIdx, chainTopCoeff, chainTopIdx	4
Theorems Iic_chainBotCoeff_eq, Iic_chainTopCoeff_eq, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, chainBotCoeff_add_chainTopCoeff_le_three, chainBotCoeff_chainTopIdx, chainBotCoeff_eq_sSup, chainBotCoeff_eq_zero_iff, chainBotCoeff_of_add, chainBotCoeff_of_not_linearIndependent, chainBotCoeff_reflectionPerm_left, chainBotCoeff_reflectionPerm_right, chainBotCoeff_sub_chainTopCoeff, chainCoeff_chainTopIdx_aux, chainTopCoeff_chainTopIdx, chainTopCoeff_eq_sSup, chainTopCoeff_eq_zero_iff, chainTopCoeff_of_add, chainTopCoeff_of_not_linearIndependent, chainTopCoeff_of_sub, chainTopCoeff_reflectionPerm_left, chainTopCoeff_reflectionPerm_right, chainTopCoeff_sub_chainBotCoeff, coe_chainBotCoeff_eq_sSup, coe_chainTopCoeff_eq_sSup, one_le_chainBotCoeff_of_root_add_mem, one_le_chainTopCoeff_of_root_add_mem, root_add_nsmul_mem_range_iff_le_chainTopCoeff, root_add_zsmul_mem_range_iff, root_chainBotIdx, root_chainTopIdx, root_sub_nsmul_mem_range_iff_le_chainBotCoeff, root_sub_zsmul_mem_range_iff, setOf_root_add_zsmul_eq_Icc_of_linearIndependent, setOf_root_add_zsmul_mem_eq_Icc, setOf_root_sub_zsmul_mem_eq_Icc	35
Total	39

RootPairing

Definitions

Name	Category	Theorems
chainBotCoeff 📖	CompOp	28 math math: chainTopCoeff_reflectionPerm_right, coe_chainBotCoeff_eq_sSup, setOf_root_add_zsmul_mem_eq_Icc, setOf_root_sub_zsmul_mem_eq_Icc, chainBotCoeff_add_chainTopCoeff_le_three, chainBotCoeff_reflectionPerm_right, Base.chainBotCoeff_eq_zero, chainBotCoeff_mul_chainTopCoeff, chainCoeff_chainTopIdx_aux, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, root_sub_nsmul_mem_range_iff_le_chainBotCoeff, chainBotCoeff_of_not_linearIndependent, one_le_chainBotCoeff_of_root_add_mem, chainTopCoeff_reflectionPerm_left, chainBotCoeff_of_add, chainBotCoeff_eq_sSup, GeckConstruction.e_lie_v_ne, root_add_zsmul_mem_range_iff, chainBotCoeff_chainTopIdx, chainBotCoeff_add_chainTopCoeff_le_two, Iic_chainBotCoeff_eq, chainBotCoeff_if_one_zero, chainTopCoeff_sub_chainBotCoeff, root_sub_zsmul_mem_range_iff, chainBotCoeff_eq_zero_iff, chainBotCoeff_reflectionPerm_left, root_chainBotIdx, chainBotCoeff_sub_chainTopCoeff
chainBotIdx 📖	CompOp	1 math math: root_chainBotIdx
chainTopCoeff 📖	CompOp	31 math math: chainTopCoeff_reflectionPerm_right, Iic_chainTopCoeff_eq, setOf_root_add_zsmul_mem_eq_Icc, chainTopCoeff_of_not_linearIndependent, setOf_root_sub_zsmul_mem_eq_Icc, chainBotCoeff_add_chainTopCoeff_le_three, chainBotCoeff_reflectionPerm_right, one_le_chainTopCoeff_of_root_add_mem, coe_chainTopCoeff_eq_sSup, chainTopCoeff_of_sub, chainBotCoeff_mul_chainTopCoeff, chainTopCoeff_eq_zero_iff, chainCoeff_chainTopIdx_aux, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, chainTopCoeff_reflectionPerm_left, GeckConstruction.f_lie_v_ne, root_add_zsmul_mem_range_iff, chainBotCoeff_chainTopIdx, chainTopCoeff_chainTopIdx, chainBotCoeff_add_chainTopCoeff_le_two, Base.cartanMatrix_eq_neg_chainTopCoeff, chainTopCoeff_eq_sSup, chainTopCoeff_if_one_zero, chainTopCoeff_of_add, chainTopCoeff_sub_chainBotCoeff, root_sub_zsmul_mem_range_iff, chainBotCoeff_reflectionPerm_left, root_chainTopIdx, chainBotCoeff_sub_chainTopCoeff, root_add_nsmul_mem_range_iff_le_chainTopCoeff, Base.chainTopCoeff_eq_of_ne
chainTopIdx 📖	CompOp	5 math math: chainCoeff_chainTopIdx_aux, chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, chainBotCoeff_chainTopIdx, chainTopCoeff_chainTopIdx, root_chainTopIdx

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iic_chainBotCoeff_eq 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set.Iic Nat.instPreorder chainBotCoeff setOf Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	Set.ext root_sub_nsmul_mem_range_iff_le_chainBotCoeff
Iic_chainTopCoeff_eq 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set.Iic Nat.instPreorder chainTopCoeff setOf Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Set.ext root_add_nsmul_mem_range_iff_le_chainTopCoeff
chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainBotCoeff chainTopCoeff pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing chainTopIdx	—	root_chainTopIdx add_comm natCast_zsmul LinearIndependent.pair_add_smul_right_iff Int.instIsDomain AddGroup.int_smulCommClass AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero chainBotCoeff_chainTopIdx Nat.cast_add chainTopCoeff_chainTopIdx CharP.cast_eq_zero CharP.ofCharZero Int.instCharZero sub_zero chainBotCoeff_sub_chainTopCoeff
chainBotCoeff_add_chainTopCoeff_le_three 📖	mathematical	—	chainBotCoeff chainTopCoeff	—	Nat.cast_add Nat.instAtLeastTwoHAddOfNat Nat.cast_ofNat chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero Int.instIsOrderedAddMonoid chainBotCoeff_of_not_linearIndependent chainTopCoeff_of_not_linearIndependent add_zero Nat.instCanonicallyOrderedAdd
chainBotCoeff_chainTopIdx 📖	mathematical	—	chainBotCoeff chainTopIdx chainTopCoeff	—	chainCoeff_chainTopIdx_aux
chainBotCoeff_eq_sSup 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainBotCoeff SupSet.sSup Nat.instSupSet setOf Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid	—	Iic_chainBotCoeff_eq csSup_Iic
chainBotCoeff_eq_zero_iff 📖	mathematical	—	chainBotCoeff LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Nat.instCanonicallyOrderedAdd le_refl Iic_chainBotCoeff_eq one_smul root_sub_nsmul_mem_range_iff_le_chainBotCoeff not_le Set.mem_Iic zero_nsmul sub_zero Function.instEmbeddingLikeEmbedding chainBotCoeff_of_not_linearIndependent
chainBotCoeff_of_add 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	chainBotCoeff	—	add_comm Nat.cast_injective Int.instCharZero Nat.cast_add Nat.cast_one coe_chainBotCoeff_eq_sSup Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat covariant_swap_add_of_covariant_add Int.instAddLeftMono sub_eq_add_neg Set.image_congr Set.image_add_right setOf_root_sub_zsmul_mem_eq_Icc bddAbove_Icc OrderIso.map_csSup' zero_smul sub_zero Function.instEmbeddingLikeEmbedding OrderIso.addRight_apply
chainBotCoeff_of_not_linearIndependent 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainBotCoeff	—	setOf_root_add_zsmul_eq_Icc_of_linearIndependent
chainBotCoeff_reflectionPerm_left 📖	mathematical	—	chainBotCoeff DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm chainTopCoeff	—	le_antisymm Int.instAddLeftMono covariant_swap_add_of_covariant_add Int.instZeroLEOneClass Int.instCharZero chainTopCoeff_reflectionPerm_left
chainBotCoeff_reflectionPerm_right 📖	mathematical	—	chainBotCoeff DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm chainTopCoeff	—	le_antisymm Int.instAddLeftMono covariant_swap_add_of_covariant_add Int.instZeroLEOneClass Int.instCharZero chainTopCoeff_reflectionPerm_right
chainBotCoeff_sub_chainTopCoeff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainBotCoeff chainTopCoeff pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	RingHomInvPair.ids root_chainBotIdx map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass algebraMap_pairingIn eq_intCast RingHom.instRingHomClass map_nsmul reflection_apply_self smul_neg sub_neg_eq_add Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.sub_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 AddCommGroup.intIsScalarTower 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 Nat.cast_one Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_mul Int.cast_mul Int.cast_sub Int.cast_natCast Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one root_reflectionPerm Set.mem_range_self Set.mem_Icc root_add_zsmul_mem_range_iff le_antisymm chainBotCoeff_reflectionPerm_left chainTopCoeff_reflectionPerm_left pairingIn_reflectionPerm_self_right instFaithfulSMulIntOfCharZero
chainCoeff_chainTopIdx_aux 📖	mathematical	—	chainBotCoeff chainTopIdx chainTopCoeff	—	root_chainTopIdx add_comm natCast_zsmul LinearIndependent.pair_add_smul_right_iff Int.instIsDomain AddGroup.int_smulCommClass AddCommGroup.intIsScalarTower instIsTorsionFreeIntOfIsAddTorsionFree IsAddTorsionFree.of_isCancelMulZero_charZero IsDomain.toIsCancelMulZero Set.ext add_assoc Set.image_add_left neg_neg add_smul Set.mem_setOf_eq root_add_zsmul_mem_range_iff Nat.cast_zero Int.instCharZero neg_add_rev neg_eq_iff_eq_neg Set.Icc_eq_Icc_iff neg_add_cancel Set.image_const_add_Icc IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing AddGroup.existsAddOfLE chainBotCoeff_of_not_linearIndependent chainTopCoeff_of_not_linearIndependent zero_nsmul add_zero
chainTopCoeff_chainTopIdx 📖	mathematical	—	chainTopCoeff chainTopIdx	—	chainCoeff_chainTopIdx_aux
chainTopCoeff_eq_sSup 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainTopCoeff SupSet.sSup Nat.instSupSet setOf Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Iic_chainTopCoeff_eq csSup_Iic
chainTopCoeff_eq_zero_iff 📖	mathematical	—	chainTopCoeff LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	chainBotCoeff_reflectionPerm_left RingHomInvPair.ids root_reflectionPerm reflection_apply_self sub_neg_eq_add
chainTopCoeff_of_add 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	chainTopCoeff	—	add_comm Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg chainTopCoeff_of_sub
chainTopCoeff_of_not_linearIndependent 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainTopCoeff	—	setOf_root_add_zsmul_eq_Icc_of_linearIndependent
chainTopCoeff_of_sub 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	chainTopCoeff	—	RingHomInvPair.ids root_reflectionPerm reflection_apply_self sub_eq_add_neg chainBotCoeff_reflectionPerm_left chainBotCoeff_of_add
chainTopCoeff_reflectionPerm_left 📖	mathematical	—	chainTopCoeff DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm chainBotCoeff	—	le_antisymm Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero
chainTopCoeff_reflectionPerm_right 📖	mathematical	—	chainTopCoeff DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reflectionPerm chainBotCoeff	—	le_antisymm Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero
chainTopCoeff_sub_chainBotCoeff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainTopCoeff chainBotCoeff pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	chainBotCoeff_sub_chainTopCoeff neg_sub
coe_chainBotCoeff_eq_sSup 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainBotCoeff SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder setOf Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul	—	setOf_root_sub_zsmul_mem_eq_Icc csSup_Icc
coe_chainTopCoeff_eq_sSup 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	chainTopCoeff SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder setOf Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	setOf_root_add_zsmul_mem_eq_Icc csSup_Icc
one_le_chainBotCoeff_of_root_add_mem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	chainBotCoeff	—	linearIndependent_of_sub_mem_range_root' root_sub_nsmul_mem_range_iff_le_chainBotCoeff one_smul neg_mem_range_root_iff neg_sub
one_le_chainTopCoeff_of_root_add_mem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	chainTopCoeff	—	linearIndependent_of_add_mem_range_root' root_add_nsmul_mem_range_iff_le_chainTopCoeff one_smul add_comm
root_add_nsmul_mem_range_iff_le_chainTopCoeff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup chainTopCoeff	—	setOf_root_add_zsmul_eq_Icc_of_linearIndependent Set.mem_Icc natCast_zsmul
root_add_zsmul_mem_range_iff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder chainBotCoeff chainTopCoeff	—	natCast_zsmul root_add_nsmul_mem_range_iff_le_chainTopCoeff Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero neg_smul root_sub_nsmul_mem_range_iff_le_chainBotCoeff covariant_swap_add_of_covariant_add
root_chainBotIdx 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root chainBotIdx SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid chainBotCoeff	—	root_sub_nsmul_mem_range_iff_le_chainBotCoeff le_refl setOf_root_add_zsmul_eq_Icc_of_linearIndependent zero_smul sub_zero
root_chainTopIdx 📖	mathematical	—	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root chainTopIdx AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup chainTopCoeff	—	root_add_nsmul_mem_range_iff_le_chainTopCoeff le_refl setOf_root_add_zsmul_eq_Icc_of_linearIndependent zero_smul add_zero
root_sub_nsmul_mem_range_iff_le_chainBotCoeff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoid.toNatSMul SubNegMonoid.toAddMonoid chainBotCoeff	—	setOf_root_add_zsmul_eq_Icc_of_linearIndependent Set.mem_Icc neg_smul natCast_zsmul
root_sub_zsmul_mem_range_iff 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder chainTopCoeff chainBotCoeff	—	sub_eq_add_neg neg_smul root_add_zsmul_mem_range_iff Set.mem_Icc
setOf_root_add_zsmul_eq_Icc_of_linearIndependent 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	setOf Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder	—	LinearIndependent.pair_iff LinearIndependent.restrict_scalars' AddCommGroup.intIsScalarTower instFaithfulSMulIntOfCharZero IsScalarTower.right zero_smul add_zero Function.instEmbeddingLikeEmbedding Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap IsAddTorsionFree.of_isTorsionFree Module.IsReflexive.to_isTorsionFree IsDomain.toIsCancelMulZero AddLeftCancelSemigroup.toIsLeftCancelAdd Function.Embedding.injective smul_left_injective Int.instIsCancelMulZero instIsTorsionFreeIntOfIsAddTorsionFree ne_zero CharZero.NeZero.two Finite.of_injective csInf_le Set.Finite.bddBelow instIsCodirectedOrder IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing instArchimedeanInt le_csSup Set.Finite.bddAbove instIsDirectedOrder Set.Nonempty.eq_Icc_iff_int 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.add_eq_eval₂ 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.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Disjoint.notMem_of_mem_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Int.instAddLeftMono contravariant_lt_of_covariant_le Int.instZeroLEOneClass Mathlib.Tactic.Contrapose.contrapose₃ Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq sub_eq_of_eq_add Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.neg_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_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.neg_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add add_smul one_smul sub_add_cancel neg_add_cancel Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Ring.mul_one lt_sub_right_of_add_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sub_smul sub_sub_cancel_left root_add_root_mem_of_pairingIn_neg Mathlib.Tactic.Contrapose.contrapose₁ FaithfulSMul.algebraMap_injective algebraMap_pairingIn map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass root_coroot'_eq_pairing Nat.instAtLeastTwoHAddOfNat Algebra.to_smulCommClass SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LinearMap.map_smul_of_tower LinearMap.CompatibleSMul.intModule pairing_same zsmul_eq_mul eq_intCast Int.cast_ofNat root_sub_root_mem_of_pairingIn_pos
setOf_root_add_zsmul_mem_eq_Icc 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	setOf Set Set.instMembership Set.range AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder chainBotCoeff chainTopCoeff	—	Set.ext root_add_zsmul_mem_range_iff
setOf_root_sub_zsmul_mem_eq_Icc 📖	mathematical	LinearIndependent Matrix.vecCons DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	setOf Set Set.instMembership Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SubNegMonoid.toZSMul Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder chainTopCoeff chainBotCoeff	—	Set.ext root_sub_zsmul_mem_range_iff Set.mem_setOf_eq

---

← Back to Index