Reduced

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

Statistics

Metric	Count
Definitions `IsReduced`	1
Theorems `eq_or_eq_neg`, `linearIndependent`, `linearIndependent_iff`, `coxeterWeightIn_eq_four_iff_not_linearIndependent`, `coxeterWeightIn_ne_four`, `coxeterWeight_eq_four_iff_not_linearIndependent`, `coxeterWeight_ne_four_of_linearIndependent`, `infinite_of_linearIndependent_coxeterWeight_four`, `instFlipIsReduced`, `isReduced_iff`, `isReduced_iff'`, `linearIndependent_iff_coxeterWeightIn_ne_four`, `linearIndependent_iff_coxeterWeight_ne_four`, `linearIndependent_of_add_mem_range_root`, `linearIndependent_of_add_mem_range_root'`, `linearIndependent_of_sub_mem_range_root`, `linearIndependent_of_sub_mem_range_root'`, `nsmul_notMem_range_root`, `pairingIn_neg_one_neg_four_iff`, `pairingIn_neg_two_neg_two_iff`, `pairingIn_one_four_iff`, `pairingIn_two_two_iff`, `pairing_neg_one_neg_four_iff`, `pairing_neg_one_neg_four_iff'`, `pairing_neg_two_neg_two_iff`, `pairing_one_four_iff`, `pairing_one_four_iff'`, `pairing_smul_root_eq_of_not_linearIndependent`, `pairing_two_two_iff`	29
Total	30

RootPairing

Definitions

Name	Category	Theorems
`IsReduced` 📖	CompData	7 math math: `LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `IsG2.toIsReduced`, `isReduced_iff'`, `EmbeddedG2.toIsReduced`, `isReduced_iff`, `instFlipIsReduced`, `IsNotG2.toIsReduced`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coxeterWeightIn_eq_four_iff_not_linearIndependent` 📖	mathematical	—	`coxeterWeightIn` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `linearIndependent_iff_coxeterWeightIn_ne_four`
`coxeterWeightIn_ne_four` 📖	—	—	—	—	`Nat.instAtLeastTwoHAddOfNat` `coxeterWeightIn_eq_four_iff_not_linearIndependent` `IsReduced.linearIndependent`
`coxeterWeight_eq_four_iff_not_linearIndependent` 📖	mathematical	—	`coxeterWeight` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `linearIndependent_iff_coxeterWeight_ne_four`
`coxeterWeight_ne_four_of_linearIndependent` 📖	—	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—	`Nat.instAtLeastTwoHAddOfNat` `infinite_of_linearIndependent_coxeterWeight_four` `not_finite`
`infinite_of_linearIndependent_coxeterWeight_four` 📖	mathematical	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `coxeterWeight` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`Infinite`	—	`Nat.instAtLeastTwoHAddOfNat` `Set.infinite_range_iff` `Function.Embedding.injective` `Set.Infinite.mono` `RingHomInvPair.ids` `RingHomCompTriple.ids` `SMulCommClass.symm` `Algebra.to_smulCommClass` `coroot_root_two` `Set.range_subset_iff` `Function.IsFixedPt.image_iterate` `Set.BijOn.image_eq` `Set.BijOn.comp` `Module.bijOn_reflection_of_mapsTo` `mapsTo_reflection_root` `Set.mem_image_of_mem` `Set.mem_range_self` `Module.infinite_range_reflection_reflection_iterate_iff` `coroot_root_eq_pairing` `mul_comm` `coxeterWeight.eq_1` `sub_eq_zero` `sub_eq_add_neg` `neg_smul` `two_ne_zero` `LinearIndependent.pair_iff`
`instFlipIsReduced` 📖	mathematical	—	`IsReduced` `flip`	—	`eq_or_ne` `RingHomInvPair.ids` `root_eq_neg_iff` `Mathlib.Tactic.Push.not_and_eq` `IsReduced.linearIndependent_iff` `instNontrivialOfCharZero` `Nat.instAtLeastTwoHAddOfNat` `coxeterWeight_eq_four_iff_not_linearIndependent` `coxeterWeight_flip` `coroot_reflectionPerm` `coreflection_apply_self`
`isReduced_iff` 📖	mathematical	—	`IsReduced` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`isReduced_iff'` 📖	mathematical	—	`IsReduced` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`isReduced_iff` `Function.instEmbeddingLikeEmbedding` `eq_or_ne`
`linearIndependent_iff_coxeterWeightIn_ne_four` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `linearIndependent_iff_coxeterWeight_ne_four` `algebraMap_coxeterWeightIn` `map_ofNat` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective`
`linearIndependent_iff_coxeterWeight_ne_four` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`IsAddTorsionFree.of_isTorsionFree` `IsDomain.toIsCancelMulZero` `Nat.instAtLeastTwoHAddOfNat` `coxeterWeight_ne_four_of_linearIndependent` `CharZero.NeZero.two` `Mathlib.Tactic.Contrapose.contrapose₂` `pairing_smul_root_eq_of_not_linearIndependent` `LinearIndependent.pair_symm_iff` `SemigroupAction.mul_smul` `SMulCommClass.smul_comm` `smulCommClass_self` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `smul_left_injective` `ne_zero`
`linearIndependent_of_add_mem_range_root` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`IsReduced.linearIndependent` `nsmul_notMem_range_root` `Nat.instAtLeastTwoHAddOfNat` `two_smul` `zero_notMem_range_root` `CharZero.NeZero.two` `neg_add_cancel`
`linearIndependent_of_add_mem_range_root'` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Module.IsReflexive.of_isPerfPair` `isPerfPair_toLinearMap` `IsAddTorsionFree.of_isTorsionFree` `Module.IsReflexive.to_isTorsionFree` `IsDomain.toIsCancelMulZero` `linearIndependent_of_add_mem_range_root`
`linearIndependent_of_sub_mem_range_root` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`linearIndependent_of_add_mem_range_root` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `sub_eq_add_neg`
`linearIndependent_of_sub_mem_range_root'` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.IsReflexive.of_isPerfPair` `isPerfPair_toLinearMap` `IsAddTorsionFree.of_isTorsionFree` `Module.IsReflexive.to_isTorsionFree` `IsDomain.toIsCancelMulZero` `linearIndependent_of_sub_mem_range_root`
`nsmul_notMem_range_root` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`one_smul` `neg_smul` `Nat.cast_smul_eq_nsmul` `add_neg_cancel` `NeZero.charZero_one` `instNontrivialOfCharZero` `natCast_zsmul` `Nat.AtLeastTwo.prop` `smul_left_injective` `Int.instIsCancelMulZero` `instIsTorsionFreeIntOfIsAddTorsionFree` `ne_zero` `CharZero.NeZero.two`
`pairingIn_neg_one_neg_four_iff` 📖	mathematical	—	`pairingIn` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `pairing_neg_one_neg_four_iff` `algebraMap_pairingIn` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_ofNat` `map_neg` `RingHomClass.toAddMonoidHomClass` `FaithfulSMul.algebraMap_injective`
`pairingIn_neg_two_neg_two_iff` 📖	mathematical	—	`pairingIn` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root`	—	`Nat.instAtLeastTwoHAddOfNat` `pairing_neg_two_neg_two_iff` `algebraMap_pairingIn` `map_ofNat` `RingHom.instRingHomClass` `RingHomClass.toAddMonoidHomClass` `FaithfulSMul.algebraMap_injective`
`pairingIn_one_four_iff` 📖	mathematical	—	`pairingIn` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `pairing_one_four_iff` `algebraMap_pairingIn` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_ofNat` `FaithfulSMul.algebraMap_injective`
`pairingIn_two_two_iff` 📖	mathematical	—	`pairingIn` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `pairing_two_two_iff` `algebraMap_pairingIn` `map_ofNat` `RingHom.instRingHomClass` `FaithfulSMul.algebraMap_injective`
`pairing_neg_one_neg_four_iff` 📖	mathematical	—	`pairing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`pairing_neg_one_neg_four_iff'` `smul_right_injective` `Nat.instAtLeastTwoHAddOfNat` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `IsDomain.toIsCancelMulZero` `two_ne_zero` `CharZero.NeZero.two`
`pairing_neg_one_neg_four_iff'` 📖	mathematical	`IsSMulRegular` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`pairing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `neg_smul` `pairing_reflectionPerm_self_right` `pairing_reflectionPerm_self_left` `RingHomInvPair.ids` `root_reflectionPerm` `reflection_apply_self` `pairing_one_four_iff'`
`pairing_neg_two_neg_two_iff` 📖	mathematical	—	`pairing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root`	—	`Nat.instAtLeastTwoHAddOfNat` `pairing_reflectionPerm_self_left` `pairing_reflectionPerm_self_right` `pairing_two_two_iff`
`pairing_one_four_iff` 📖	mathematical	—	`pairing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`pairing_one_four_iff'` `smul_right_injective` `Nat.instAtLeastTwoHAddOfNat` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `IsDomain.toIsCancelMulZero` `two_ne_zero` `CharZero.NeZero.two`
`pairing_one_four_iff'` 📖	mathematical	`IsSMulRegular` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	`pairing` `AddMonoidWithOne.toOne` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `IsAddTorsionFree.of_isTorsionFree` `IsDomain.toIsCancelMulZero` `coxeterWeight_eq_four_iff_not_linearIndependent` `coxeterWeight.eq_1` `one_mul` `pairing_smul_root_eq_of_not_linearIndependent` `CharZero.NeZero.two` `smul_right_injective` `two_ne_zero` `SemigroupAction.mul_smul` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_mul` `pairing.eq_1` `coroot_eq_smul_coroot_iff` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `pairing_same` `Mathlib.Meta.NormNum.IsNat.to_eq` `mul_one`
`pairing_smul_root_eq_of_not_linearIndependent` 📖	mathematical	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `pairing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `LinearIndependent.pair_iff` `eq_or_ne` `smul_eq_zero_iff_left` `IsDomain.toIsCancelMulZero` `ne_zero` `zero_smul` `zero_add` `add_zero` `neg_smul` `eq_neg_iff_add_eq_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `pairing_same` `Algebra.to_smulCommClass` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `smul_right_injective` `neg_ne_zero` `smul_smul` `neg_mul` `SMulCommClass.smul_comm` `smulCommClass_self` `mul_comm`
`pairing_two_two_iff` 📖	mathematical	—	`pairing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `coxeterWeight_eq_four_iff_not_linearIndependent` `coxeterWeight.eq_1` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `pairing_smul_root_eq_of_not_linearIndependent` `CharZero.NeZero.two` `Function.Embedding.injective` `smul_right_injective` `IsDomain.toIsCancelMulZero` `two_ne_zero` `pairing_same`

RootPairing.IsReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_eq_neg` 📖	mathematical	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`linearIndependent` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`eq_or_eq_neg` `Function.instEmbeddingLikeEmbedding`
`linearIndependent_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `RootPairing.root` `Matrix.vecEmpty` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `eq_or_ne` `one_smul` `neg_smul` `add_neg_cancel` `NeZero.one` `smul_neg` `neg_add_cancel` `LinearIndependent.pair_iff` `linearIndependent`

---

← Back to Index