G2

📁 Source: Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean

Statistics

Metric	Count
Definitions G2, EmbeddedG2, allCoeffs, allRoots, basis, indexEquivAllRoots, long, longRoot, ofPairingInThree, short, shortAddLong, shortAddLongRoot, shortRoot, threeShortAddLong, threeShortAddLongRoot, threeShortAddTwoLong, threeShortAddTwoLongRoot, twoShortAddLong, twoShortAddLongRoot, IsG2, toEmbeddedG2, IsNotG2	22
Theorems allRoots_eq_map_allCoeffs, allRoots_nodup, allRoots_subset_range_root, card_index_eq_twelve, indexEquivAllRoots_apply_coe, indexEquivAllRoots_symm_apply, instIsG2OfIsIrreducible, isOrthogonal_short_and_long, linearIndependent_short_long, long_eq_three_mul_short, mem_allRoots, mem_span_of_mem_allRoots, ofPairingInThree_long, ofPairingInThree_short, pairingIn_long_short, pairingIn_shortAddLong_left, pairingIn_shortAddLong_right, pairingIn_short_long, pairingIn_threeShortAddLong_left, pairingIn_threeShortAddLong_right, pairingIn_threeShortAddTwoLong_left, pairingIn_threeShortAddTwoLong_right, pairingIn_twoShortAddLong_left, pairingIn_twoShortAddLong_right, pairing_long_short, pairing_short_long, setOf_index_eq_univ, shortAddLongRoot_eq, shortAddLongRoot_shortRoot, span_eq_top, threeShortAddLongRoot_eq, threeShortAddLongRoot_longRoot, threeShortAddTwoLongRoot_eq, threeShortAddTwoLongRoot_longRoot, toIsReduced, toIsValuedIn, twoShortAddLongRoot_eq, twoShortAddLongRoot_shortRoot, card_base_support_eq_two, exists_pairingIn_neg_three, nonempty, pairingIn_mem_zero_one_three, span_eq_rootSpan_int, toIsIrreducible, toIsReduced, toIsValuedIn, pairingIn_mem_zero_one_two, toIsIrreducible, toIsReduced, toIsValuedIn, chainBotCoeff_add_chainTopCoeff_le_two, chainBotCoeff_if_one_zero, chainTopCoeff_if_one_zero, isG2_iff, isNotG2_iff, not_isG2_iff_isNotG2, pairingIn_le_zero_of_root_add_mem, zero_le_pairingIn_of_root_sub_mem	58
Total	80

EisensteinSeries

Definitions

Name	Category	Theorems
G2 📖	CompOp	7 math math: G2_slash_action, G2_eq_tsum_symmetricIco, G2_S_transform, tendsto_double_sum_S_act, G2_eq_tsum_cexp, tsum_symmetricIco_tsum_eq_S_act, G2_T_transform

RootPairing

Definitions

Name	Category	Theorems
EmbeddedG2 📖	CompData	—
IsG2 📖	CompData	3 math math: EmbeddedG2.instIsG2OfIsIrreducible, isG2_iff, not_isG2_iff_isNotG2
IsNotG2 📖	CompData	3 math math: not_isG2_iff_isNotG2, chainBotCoeff_mul_chainTopCoeff.isNotG2, isNotG2_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chainBotCoeff_add_chainTopCoeff_le_two 📖	mathematical	—	chainBotCoeff IsNotG2.toIsValuedIn chainTopCoeff	—	IsNotG2.toIsValuedIn Nat.cast_add Nat.instAtLeastTwoHAddOfNat Nat.cast_ofNat chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx IsNotG2.pairingIn_mem_zero_one_two Int.instIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero chainBotCoeff_of_not_linearIndependent chainTopCoeff_of_not_linearIndependent add_zero Nat.instCanonicallyOrderedAdd
chainBotCoeff_if_one_zero 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	chainBotCoeff IsNotG2.toIsValuedIn pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap linearIndependent_of_add_mem_range_root' IsNotG2.toIsReduced IsNotG2.toIsValuedIn chainBotCoeff_add_chainTopCoeff_le_two one_le_chainTopCoeff_of_root_add_mem eq_or_ne pairingIn_eq_zero_iff Module.IsReflexive.to_isTorsionFree CharZero.NeZero.two instFaithfulSMulIntOfCharZero chainBotCoeff_sub_chainTopCoeff Int.instCharZero
chainTopCoeff_if_one_zero 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	chainTopCoeff IsNotG2.toIsValuedIn pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	RingHomInvPair.ids root_reflectionPerm reflection_apply_self IsNotG2.toIsValuedIn chainBotCoeff_reflectionPerm_right pairingIn_reflectionPerm_self_right instFaithfulSMulIntOfCharZero chainBotCoeff_if_one_zero
isG2_iff 📖	mathematical	—	IsG2 pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	IsG2.exists_pairingIn_neg_three
isNotG2_iff 📖	mathematical	—	IsNotG2 Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	IsNotG2.pairingIn_mem_zero_one_two
not_isG2_iff_isNotG2 📖	mathematical	—	IsG2 IsNotG2	—	pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed pairingIn_reflectionPerm_self_left instFaithfulSMulIntOfCharZero Int.instCharZero Nat.instAtLeastTwoHAddOfNat
pairingIn_le_zero_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	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing IsNotG2.toIsValuedIn	—	linearIndependent_of_add_mem_range_root' IsNotG2.toIsReduced add_comm IsNotG2.toIsValuedIn chainBotCoeff_add_chainTopCoeff_le_two root_add_nsmul_mem_range_iff_le_chainTopCoeff one_smul chainBotCoeff_sub_chainTopCoeff
zero_le_pairingIn_of_root_sub_mem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing IsNotG2.toIsValuedIn	—	RingHomInvPair.ids root_reflectionPerm reflection_apply_self IsNotG2.toIsValuedIn pairingIn_reflectionPerm_self_right instFaithfulSMulIntOfCharZero Int.instAddLeftMono pairingIn_le_zero_of_root_add_mem

RootPairing.EmbeddedG2

Definitions

Name	Category	Theorems
allCoeffs 📖	CompOp	1 math math: allRoots_eq_map_allCoeffs
allRoots 📖	CompOp	6 math math: indexEquivAllRoots_symm_apply, allRoots_eq_map_allCoeffs, indexEquivAllRoots_apply_coe, allRoots_nodup, allRoots_subset_range_root, mem_allRoots
basis 📖	CompOp	—
indexEquivAllRoots 📖	CompOp	2 math math: indexEquivAllRoots_symm_apply, indexEquivAllRoots_apply_coe
long 📖	CompOp	15 math math: pairingIn_threeShortAddLong_right, isOrthogonal_short_and_long, pairingIn_twoShortAddLong_left, pairingIn_threeShortAddTwoLong_right, pairingIn_long_short, pairingIn_threeShortAddLong_left, pairing_long_short, pairingIn_short_long, pairingIn_twoShortAddLong_right, pairingIn_threeShortAddTwoLong_left, pairing_short_long, pairingIn_shortAddLong_left, ofPairingInThree_long, setOf_index_eq_univ, pairingIn_shortAddLong_right
longRoot 📖	CompOp	11 math math: mem_span_of_mem_allRoots, twoShortAddLongRoot_eq, long_eq_three_mul_short, allRoots_eq_map_allCoeffs, linearIndependent_short_long, threeShortAddTwoLongRoot_eq, span_eq_top, threeShortAddLongRoot_longRoot, threeShortAddTwoLongRoot_longRoot, threeShortAddLongRoot_eq, shortAddLongRoot_eq
ofPairingInThree 📖	CompOp	2 math math: ofPairingInThree_short, ofPairingInThree_long
short 📖	CompOp	15 math math: pairingIn_threeShortAddLong_right, isOrthogonal_short_and_long, pairingIn_twoShortAddLong_left, pairingIn_threeShortAddTwoLong_right, pairingIn_long_short, pairingIn_threeShortAddLong_left, pairing_long_short, pairingIn_short_long, pairingIn_twoShortAddLong_right, ofPairingInThree_short, pairingIn_threeShortAddTwoLong_left, pairing_short_long, pairingIn_shortAddLong_left, setOf_index_eq_univ, pairingIn_shortAddLong_right
shortAddLong 📖	CompOp	3 math math: pairingIn_shortAddLong_left, setOf_index_eq_univ, pairingIn_shortAddLong_right
shortAddLongRoot 📖	CompOp	2 math math: shortAddLongRoot_shortRoot, shortAddLongRoot_eq
shortRoot 📖	CompOp	11 math math: mem_span_of_mem_allRoots, shortAddLongRoot_shortRoot, twoShortAddLongRoot_eq, long_eq_three_mul_short, allRoots_eq_map_allCoeffs, linearIndependent_short_long, threeShortAddTwoLongRoot_eq, twoShortAddLongRoot_shortRoot, span_eq_top, threeShortAddLongRoot_eq, shortAddLongRoot_eq
threeShortAddLong 📖	CompOp	3 math math: pairingIn_threeShortAddLong_right, pairingIn_threeShortAddLong_left, setOf_index_eq_univ
threeShortAddLongRoot 📖	CompOp	2 math math: threeShortAddLongRoot_longRoot, threeShortAddLongRoot_eq
threeShortAddTwoLong 📖	CompOp	3 math math: pairingIn_threeShortAddTwoLong_right, pairingIn_threeShortAddTwoLong_left, setOf_index_eq_univ
threeShortAddTwoLongRoot 📖	CompOp	2 math math: threeShortAddTwoLongRoot_eq, threeShortAddTwoLongRoot_longRoot
twoShortAddLong 📖	CompOp	3 math math: pairingIn_twoShortAddLong_left, pairingIn_twoShortAddLong_right, setOf_index_eq_univ
twoShortAddLongRoot 📖	CompOp	2 math math: twoShortAddLongRoot_eq, twoShortAddLongRoot_shortRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
allRoots_eq_map_allCoeffs 📖	mathematical	—	allRoots DFunLike.coe LinearMap Int.instSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.Function.module Semiring.toModule AddCommGroup.toIntModule LinearMap.instFunLike Fintype.linearCombination Fin.fintype Matrix.vecCons shortRoot longRoot Matrix.vecEmpty allCoeffs	—	Nat.instAtLeastTwoHAddOfNat Finset.sum_congr Int.cast_smul_eq_zsmul Fin.sum_univ_two Int.cast_zero zero_smul Matrix.cons_val_fin_one Int.cast_one one_smul zero_add Int.cast_neg neg_smul add_zero Int.cast_ofNat shortAddLongRoot_eq neg_add twoShortAddLongRoot_eq threeShortAddLongRoot_eq threeShortAddTwoLongRoot_eq
allRoots_nodup 📖	mathematical	—	allRoots	—	linearIndependent_iff_injective_fintypeLinearCombination LinearIndependent.restrict_scalars' AddCommGroup.intIsScalarTower instFaithfulSMulIntOfCharZero IsScalarTower.right linearIndependent_short_long allRoots_eq_map_allCoeffs List.nodup_map_iff
allRoots_subset_range_root 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike List.toFinset allRoots Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	List.toFinset_cons Finset.instLawfulSingleton Finset.coe_insert Finset.coe_singleton Set.mem_insert_iff Function.instEmbeddingLikeEmbedding
card_index_eq_twelve 📖	mathematical	—	Nat.card	—	Nat.card_eq_fintype_card Fintype.card_coe List.toFinset_card_of_nodup allRoots_nodup zero_add Nat.card_congr
indexEquivAllRoots_apply_coe 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike List.toFinset allRoots DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike indexEquivAllRoots Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	—
indexEquivAllRoots_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Finset SetLike.instMembership Finset.instSetLike List.toFinset allRoots EquivLike.toFunLike Equiv.instEquivLike Equiv.symm indexEquivAllRoots Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	—
instIsG2OfIsIrreducible 📖	mathematical	—	RootPairing.IsG2	—	toIsValuedIn toIsReduced pairingIn_long_short
isOrthogonal_short_and_long 📖	mathematical	allRoots DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root	RootPairing.IsOrthogonal short long	—	toIsValuedIn RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' toIsReduced pairingIn_shortAddLong_right pairingIn_shortAddLong_left pairingIn_twoShortAddLong_right pairingIn_twoShortAddLong_left pairingIn_threeShortAddLong_right pairingIn_threeShortAddLong_left pairingIn_threeShortAddTwoLong_right pairingIn_threeShortAddTwoLong_left Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap CharZero.NeZero.two Module.IsReflexive.to_isTorsionFree RootPairing.algebraMap_pairingIn eq_intCast RingHom.instRingHomClass
linearIndependent_short_long 📖	mathematical	—	LinearIndependent Matrix.vecCons shortRoot longRoot Matrix.vecEmpty CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap toIsValuedIn Nat.instAtLeastTwoHAddOfNat RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four Module.IsReflexive.to_isTorsionFree instFaithfulSMulIntOfCharZero pairingIn_short_long pairingIn_long_short mul_neg neg_mul one_mul neg_neg Int.instCharZero
long_eq_three_mul_short 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form longRoot Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat shortRoot	—	Nat.instAtLeastTwoHAddOfNat pairing_short_long neg_mul one_mul pairing_long_short RootPairing.InvariantForm.pairing_mul_eq_pairing_mul_swap
mem_allRoots 📖	mathematical	—	allRoots DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	isOrthogonal_short_and_long RootPairing.IsG2.toIsValuedIn instIsG2OfIsIrreducible Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap LinearMap.ext span_eq_top Submodule.span_induction Function.instEmbeddingLikeEmbedding CharZero.NeZero.two RootPairing.InvariantForm.apply_root_root_zero_iff RootPairing.isOrthogonal_iff_pairing_eq_zero Module.IsReflexive.to_isTorsionFree map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass add_zero map_smul SemilinearMapClass.toMulActionSemiHomClass MulZeroClass.mul_zero Nat.instAtLeastTwoHAddOfNat RootPairing.pairing_same LinearMap.congr_fun
mem_span_of_mem_allRoots 📖	mathematical	allRoots	Submodule Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule SetLike.instMembership Submodule.setLike Submodule.span Set Set.instInsert longRoot Set.instSingletonSet shortRoot	—	Matrix.range_cons Matrix.range_empty Set.union_empty Set.union_singleton allRoots_eq_map_allCoeffs
ofPairingInThree_long 📖	mathematical	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	long ofPairingInThree DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike RootPairing.reflectionPerm	—	—
ofPairingInThree_short 📖	mathematical	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	short ofPairingInThree	—	—
pairingIn_long_short 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn long short	—	—
pairingIn_shortAddLong_left 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn shortAddLong short long	—	toIsValuedIn RootPairing.pairingIn_eq_add_of_root_eq_add instFaithfulSMulIntOfCharZero shortAddLongRoot_eq
pairingIn_shortAddLong_right 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn shortAddLong short long	—	Nat.instAtLeastTwoHAddOfNat toIsValuedIn Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero RootPairing.InvariantForm.ne_zero RootPairing.InvariantForm.two_mul_apply_root_root shortAddLongRoot_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass mul_add Distrib.leftDistribClass long_eq_three_mul_short shortAddLongRoot_shortRoot Mathlib.Tactic.Ring.of_eq 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.mul_pf_right 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add FaithfulSMul.algebraMap_injective RootPairing.algebraMap_pairingIn AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
pairingIn_short_long 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn short long	—	toIsValuedIn RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed toIsReduced pairingIn_long_short Int.instCharZero Nat.instAtLeastTwoHAddOfNat
pairingIn_threeShortAddLong_left 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn threeShortAddLong short long	—	toIsValuedIn RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower Nat.instAtLeastTwoHAddOfNat threeShortAddLongRoot_eq one_smul AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_smul_eq_nsmul one_mul
pairingIn_threeShortAddLong_right 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn threeShortAddLong short long	—	toIsValuedIn Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero RootPairing.InvariantForm.ne_zero Nat.instAtLeastTwoHAddOfNat RootPairing.InvariantForm.two_mul_apply_root_root threeShortAddLongRoot_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass mul_add Distrib.leftDistribClass map_smul SemilinearMapClass.toMulActionSemiHomClass smul_eq_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add long_eq_three_mul_short Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul threeShortAddLongRoot_longRoot FaithfulSMul.algebraMap_injective RootPairing.algebraMap_pairingIn AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
pairingIn_threeShortAddTwoLong_left 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn threeShortAddTwoLong short long	—	toIsValuedIn RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower Nat.instAtLeastTwoHAddOfNat threeShortAddTwoLongRoot_eq Nat.cast_smul_eq_nsmul
pairingIn_threeShortAddTwoLong_right 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn threeShortAddTwoLong short long	—	Nat.instAtLeastTwoHAddOfNat toIsValuedIn Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero RootPairing.InvariantForm.ne_zero RootPairing.InvariantForm.two_mul_apply_root_root threeShortAddTwoLongRoot_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass mul_add Distrib.leftDistribClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add long_eq_three_mul_short Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul threeShortAddTwoLongRoot_longRoot FaithfulSMul.algebraMap_injective RootPairing.algebraMap_pairingIn AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
pairingIn_twoShortAddLong_left 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn twoShortAddLong short long	—	toIsValuedIn RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower Nat.instAtLeastTwoHAddOfNat twoShortAddLongRoot_eq one_smul AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_smul_eq_nsmul one_mul
pairingIn_twoShortAddLong_right 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn twoShortAddLong short long	—	Nat.instAtLeastTwoHAddOfNat toIsValuedIn Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero RootPairing.InvariantForm.ne_zero RootPairing.InvariantForm.two_mul_apply_root_root twoShortAddLongRoot_eq map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass mul_add Distrib.leftDistribClass map_smul SemilinearMapClass.toMulActionSemiHomClass smul_eq_mul mul_assoc long_eq_three_mul_short twoShortAddLongRoot_shortRoot Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add FaithfulSMul.algebraMap_injective RootPairing.algebraMap_pairingIn AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat
pairing_long_short 📖	mathematical	—	RootPairing.pairing long short NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat toIsValuedIn RootPairing.algebraMap_pairingIn pairingIn_long_short eq_intCast RingHom.instRingHomClass Int.cast_neg Int.cast_ofNat
pairing_short_long 📖	mathematical	—	RootPairing.pairing short long NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	toIsValuedIn RootPairing.algebraMap_pairingIn pairingIn_short_long eq_intCast RingHom.instRingHomClass Int.cast_neg Int.cast_one
setOf_index_eq_univ 📖	mathematical	—	Set Set.instInsert long InvolutiveNeg.toNeg RootPairing.indexNeg short shortAddLong twoShortAddLong threeShortAddLong threeShortAddTwoLong Set.instSingletonSet Set.univ	—	Set.eq_univ_iff_forall Function.instEmbeddingLikeEmbedding mem_allRoots
shortAddLongRoot_eq 📖	mathematical	—	shortAddLongRoot AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid shortRoot longRoot	—	RingHomInvPair.ids RootPairing.root_reflectionPerm pairing_short_long neg_smul one_smul sub_neg_eq_add
shortAddLongRoot_shortRoot 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form shortAddLongRoot shortRoot	—	RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.InvariantForm.apply_reflection_reflection
span_eq_top 📖	mathematical	—	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Set.instInsert longRoot Set.instSingletonSet shortRoot Top.top Submodule Submodule.instTop	—	RootPairing.span_root_image_eq_top_of_forall_orthogonal CharZero.NeZero.two Set.ext Function.instEmbeddingLikeEmbedding Submodule.span_subset_span AddCommGroup.intIsScalarTower mem_span_of_mem_allRoots isOrthogonal_short_and_long
threeShortAddLongRoot_eq 📖	mathematical	—	threeShortAddLongRoot AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat shortRoot longRoot	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RootPairing.root_reflectionPerm pairing_long_short neg_smul sub_neg_eq_add 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₃ add_zero 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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
threeShortAddLongRoot_longRoot 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form threeShortAddLongRoot longRoot	—	RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.InvariantForm.apply_reflection_reflection
threeShortAddTwoLongRoot_eq 📖	mathematical	—	threeShortAddTwoLongRoot AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat shortRoot longRoot	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RootPairing.root_reflectionPerm pairing_long_short neg_smul sub_neg_eq_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass RootPairing.reflection_apply_self map_smul SemilinearMapClass.toMulActionSemiHomClass pairing_short_long one_smul smul_add Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.neg_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.add_eq_eval₂ zero_add Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_neg Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add
threeShortAddTwoLongRoot_longRoot 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form threeShortAddTwoLongRoot longRoot	—	RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.InvariantForm.apply_reflection_reflection
toIsReduced 📖	mathematical	—	RootPairing.IsReduced	—	—
toIsValuedIn 📖	mathematical	—	RootPairing.IsValuedIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	—
twoShortAddLongRoot_eq 📖	mathematical	—	twoShortAddLongRoot AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid 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 instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat shortRoot longRoot	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RootPairing.root_reflectionPerm pairing_short_long neg_smul one_smul sub_neg_eq_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass RootPairing.reflection_apply_self pairing_long_short Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.neg_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₃ add_zero AddCommGroup.intIsScalarTower 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 eq_intCast Int.cast_neg Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add
twoShortAddLongRoot_shortRoot 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module RootPairing.InvariantForm.form twoShortAddLongRoot shortRoot	—	RingHomInvPair.ids RootPairing.root_reflectionPerm RootPairing.InvariantForm.apply_reflection_reflection

RootPairing.IsG2

Definitions

Name	Category	Theorems
toEmbeddedG2 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_base_support_eq_two 📖	mathematical	—	Finset.card RootPairing.Base.support	—	nonempty Fintype.card_fin Module.finrank_eq_card_basis commRing_strongRankCondition instNontrivialOfCharZero toIsIrreducible RootPairing.instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible CharZero.NeZero.two Fintype.card_coe
exists_pairingIn_neg_three 📖	mathematical	—	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn	—	—
nonempty 📖	—	—	—	—	toIsValuedIn exists_pairingIn_neg_three
pairingIn_mem_zero_one_three 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	toIsValuedIn exists_pairingIn_neg_three Mathlib.Tactic.Push.not_forall_eq RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed Set.mem_insert_iff RootPairing.forall_pairingIn_eq_swap_or RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'
span_eq_rootSpan_int 📖	mathematical	Finset Finset.instMembership RootPairing.Base.support	Submodule.span Int.instSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toIntModule Set Set.instInsert DFunLike.coe Function.Embedding Function.instFunLikeEmbedding RootPairing.root Set.instSingletonSet RootPairing.rootSpan Int.instCommRing	—	Set.image_pair Finset.coe_pair Finset.eq_of_subset_of_card_le card_base_support_eq_two Finset.card_insert_of_notMem Finset.card_singleton RootPairing.Base.span_int_root_support
toIsIrreducible 📖	mathematical	—	RootPairing.IsIrreducible	—	—
toIsReduced 📖	mathematical	—	RootPairing.IsReduced	—	—
toIsValuedIn 📖	mathematical	—	RootPairing.IsValuedIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	—

RootPairing.IsNotG2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairingIn_mem_zero_one_two 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing toIsValuedIn	—	—
toIsIrreducible 📖	mathematical	—	RootPairing.IsIrreducible	—	—
toIsReduced 📖	mathematical	—	RootPairing.IsReduced	—	—
toIsValuedIn 📖	mathematical	—	RootPairing.IsValuedIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	—

---

← Back to Index