Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems apply_eq_or, apply_eq_or_aux, apply_eq_or_of_apply_ne, exists_apply_eq_or, rootLength_le_of_pairingIn_eq, rootLength_lt_of_pairingIn_notMem, coxeterWeightIn_eq_zero_iff, coxeterWeightIn_le_four, coxeterWeightIn_mem_set_of_isCrystallographic, forall_pairingIn_eq_swap_or, forall_pairing_eq_swap_or, pairingIn_eq_zero_of_add_notMem_of_sub_notMem, pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed, pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed', pairingIn_pairingIn_mem_set_of_isCrystallographic, pairingIn_pairingIn_mem_set_of_length_eq, pairingIn_pairingIn_mem_set_of_length_eq_of_ne, pairing_eq_zero_of_add_notMem_of_sub_notMem, root_add_root_mem_of_pairingIn_neg, root_mem_submodule_iff_of_add_mem_invtSubmodule, root_sub_root_mem_of_pairingIn_pos	21
Total	21

RootPairing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coxeterWeightIn_eq_zero_iff 📖	mathematical	—	coxeterWeightIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing pairingIn	—	FaithfulSMul.algebraMap_eq_zero_iff instFaithfulSMulIntOfCharZero algebraMap_pairingIn pairing_eq_zero_iff' CharZero.NeZero.two IsOrthogonal.eq_1 coxeterWeight_zero_iff_isOrthogonal algebraMap_coxeterWeightIn map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective coxeterWeightIn.eq_1 MulZeroClass.zero_mul
coxeterWeightIn_le_four 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder coxeterWeightIn instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Submodule.subset_span Set.mem_range_self Nat.instAtLeastTwoHAddOfNat RootPositiveForm.exists_pos_eq FaithfulSMul.algebraMap_injective RootPositiveForm.algebraMap_rootLength mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono four_pos IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid LinearMap.BilinForm.apply_sq_le_of_symm exists_ge_zero_eq_rootForm RootPositiveForm.algebraMap_apply_eq_form_iff RootPositiveForm.isSymm_posForm rootForm_symmetric rootForm_reflection_reflection_apply nsmul_eq_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_ofNat map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RootPositiveForm.algebraMap_posForm algebraMap_coxeterWeightIn four_smul_rootForm_sq_eq_coxeterWeight_smul mul_le_mul_iff_left₀ IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_pos
coxeterWeightIn_mem_set_of_isCrystallographic 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet coxeterWeightIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	coxeterWeight_nonneg Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower coxeterWeightIn_le_four Nat.cast_zero Nat.cast_one Int.instCharZero Int.instAddLeftMono Int.instZeroLEOneClass
forall_pairingIn_eq_swap_or 📖	mathematical	—	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Nat.instAtLeastTwoHAddOfNat algebraMap_pairingIn eq_intCast RingHom.instRingHomClass map_ofNat forall_pairing_eq_swap_or
forall_pairing_eq_swap_or 📖	mathematical	—	pairing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Int.instIsStrictOrderedRing instFaithfulSMulIntOfCharZero Nat.instAtLeastTwoHAddOfNat InvariantForm.pairing_mul_eq_pairing_mul_swap mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero InvariantForm.ne_zero Mathlib.Tactic.Push.not_forall_eq InvariantForm.apply_eq_or_of_apply_ne InvariantForm.apply_eq_or IsCancelMulZero.toIsLeftCancelMulZero CharZero.NeZero.two pairing_same mul_comm
pairingIn_eq_zero_of_add_notMem_of_sub_notMem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	le_antisymm Mathlib.Tactic.Contrapose.contrapose₂ root_sub_root_mem_of_pairingIn_pos root_add_root_mem_of_pairingIn_neg
pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap eq_or_ne Nat.instAtLeastTwoHAddOfNat pairingIn_same instFaithfulSMulIntOfCharZero Int.instCharZero pairingIn.congr_simp pairingIn_reflectionPerm_self_left pairingIn_reflectionPerm_self_right pairingIn_pairingIn_mem_set_of_isCrystallographic coxeterWeightIn_ne_four Module.IsReflexive.to_isTorsionFree mul_one one_mul mul_neg neg_neg neg_mul
pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed Nat.instAtLeastTwoHAddOfNat Module.IsReflexive.to_isTorsionFree instFaithfulSMulIntOfCharZero Function.instEmbeddingLikeEmbedding
pairingIn_pairingIn_mem_set_of_isCrystallographic 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Int.mul_mem_zero_one_two_three_four_iff algebraMap_pairingIn eq_intCast RingHom.instRingHomClass pairing_eq_zero_iff' CharZero.NeZero.two coxeterWeightIn_mem_set_of_isCrystallographic
pairingIn_pairingIn_mem_set_of_length_eq 📖	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 InvariantForm.form Function.Embedding Function.instFunLikeEmbedding root	Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	FaithfulSMul.algebraMap_injective instFaithfulSMulIntOfCharZero algebraMap_pairingIn mul_right_cancel₀ IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero InvariantForm.ne_zero InvariantForm.pairing_mul_eq_pairing_mul_swap pairingIn_pairingIn_mem_set_of_isCrystallographic Int.instCharZero Nat.instAtLeastTwoHAddOfNat
pairingIn_pairingIn_mem_set_of_length_eq_of_ne 📖	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 InvariantForm.form Function.Embedding Function.instFunLikeEmbedding root	Set Set.instMembership Set.instInsert Set.instSingletonSet pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap pairingIn_pairingIn_mem_set_of_length_eq Nat.instAtLeastTwoHAddOfNat Module.IsReflexive.to_isTorsionFree instFaithfulSMulIntOfCharZero
pairing_eq_zero_of_add_notMem_of_sub_notMem 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	pairing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	algebraMap_pairingIn pairingIn_eq_zero_of_add_notMem_of_sub_notMem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
root_add_root_mem_of_pairingIn_neg 📖	mathematical	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	pairingIn_reflectionPerm_self_right instFaithfulSMulIntOfCharZero Mathlib.Tactic.Contrapose.contrapose₄ RingHomInvPair.ids root_reflectionPerm reflection_apply_self sub_neg_eq_add root_sub_root_mem_of_pairingIn_pos
root_mem_submodule_iff_of_add_mem_invtSubmodule 📖	mathematical	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	Submodule CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike invtRootSubmodule	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne pairing_eq_zero_iff instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Algebra.to_smulCommClass root_coroot_eq_pairing map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass pairing_same add_zero two_ne_zero RingHomInvPair.ids mem_invtRootSubmodule_iff Submodule.smul_mem_iff IsScalarTower.left Submodule.sub_mem_iff_right Submodule.add_mem_iff_right add_comm
root_sub_root_mem_of_pairingIn_pos 📖	mathematical	pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	Set Set.instMembership Set.range DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	Module.IsReflexive.of_isPerfPair isPerfPair_toLinearMap IsAddTorsionFree.of_isTorsionFree Module.IsReflexive.to_isTorsionFree IsDomain.toIsCancelMulZero coxeterWeightIn_mem_set_of_isCrystallographic Nat.instAtLeastTwoHAddOfNat linearIndependent_iff_coxeterWeightIn_ne_four instFaithfulSMulIntOfCharZero coxeterWeightIn_eq_zero_iff LT.lt.ne' algebraMap_pairingIn eq_intCast RingHom.instRingHomClass RingHomInvPair.ids root_reflectionPerm one_smul reflection_apply_root neg_mem_range_root_iff neg_sub pairingIn_pairingIn_mem_set_of_isCrystallographic coxeterWeightIn_eq_four_iff_not_linearIndependent mul_one Int.instCharZero one_mul pairingIn_reflectionPerm_self_left pairingIn_same pairingIn_one_four_iff two_smul sub_add_cancel_right neg_root_mem pairingIn_two_two_iff add_sub_cancel_right Function.instEmbeddingLikeEmbedding

RootPairing.InvariantForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_or 📖	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 form Function.Embedding Function.instFunLikeEmbedding RootPairing.root Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RootPairing.exists_form_eq_form_and_form_ne_zero CharZero.NeZero.two Mathlib.Tactic.Contrapose.contrapose₄ RootPairing.algebraMap_pairingIn map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass apply_root_root_zero_iff apply_eq_or_aux
apply_eq_or_aux 📖	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 form Function.Embedding Function.instFunLikeEmbedding RootPairing.root Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed RootPairing.algebraMap_pairingIn pairing_mul_eq_pairing_mul_swap Nat.instAtLeastTwoHAddOfNat Int.cast_one one_mul eq_intCast RingHom.instRingHomClass IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero CharZero.NeZero.two RootPairing.pairing_same Int.cast_neg neg_mul Int.cast_ofNat IsCancelMulZero.toIsLeftCancelMulZero
apply_eq_or_of_apply_ne 📖	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 form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	exists_apply_eq_or
exists_apply_eq_or 📖	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 form Function.Embedding Function.instFunLikeEmbedding RootPairing.root	—	Mathlib.Tactic.Push.not_forall_eq Nat.instAtLeastTwoHAddOfNat apply_eq_or

RootPairing.RootPositiveForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rootLength_le_of_pairingIn_eq 📖	mathematical	RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	rootLength Int.instLinearOrder instFaithfulSMulIntOfCharZero AddCommGroup.toIntModule AddCommGroup.intIsScalarTower	—	RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic Int.instCharZero Nat.instAtLeastTwoHAddOfNat instFaithfulSMulIntOfCharZero AddCommGroup.intIsScalarTower pairingIn_mul_eq_pairingIn_mul_swap rootLength_pos
rootLength_lt_of_pairingIn_notMem 📖	mathematical	Set Set.instMembership Set.instInsert Set.instSingletonSet RootPairing.pairingIn Int.instCommRing Ring.toIntAlgebra CommRing.toRing	rootLength Int.instLinearOrder instFaithfulSMulIntOfCharZero AddCommGroup.toIntModule AddCommGroup.intIsScalarTower	—	RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic Int.instCharZero Nat.instAtLeastTwoHAddOfNat Module.IsReflexive.of_isPerfPair RootPairing.isPerfPair_toLinearMap Module.IsReflexive.to_isTorsionFree instFaithfulSMulIntOfCharZero Function.instEmbeddingLikeEmbedding AddCommGroup.intIsScalarTower pairingIn_mul_eq_pairingIn_mul_swap rootLength_pos

---

← Back to Index