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 zero_le_posForm 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 EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike invtRootSubmodule DFunLike.coe Function.Embedding Function.instFunLikeEmbedding root	—	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.instCommRing Int.instLinearOrder Ring.toIntAlgebra CommRing.toRing 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.instCommRing Int.instLinearOrder Ring.toIntAlgebra CommRing.toRing 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