Weight

📁 Source: Mathlib/Data/Finsupp/Weight.lean

Statistics

Metric	Count
Definitions `NonTorsionWeight`, `degree`, `weight`, `Weight`	4
Theorems `eq_zero_of_smul_eq_zero`, `ne_zero`, `degree_add`, `degree_apply`, `degree_def`, `degree_eq_sum`, `degree_eq_weight_one`, `degree_eq_zero_iff`, `degree_mono`, `degree_preimage_add`, `degree_preimage_nsmul`, `degree_single`, `degree_zero`, `exists_le_degree_eq`, `finite_of_degree_le`, `finite_of_nat_weight_le`, `image_pow_eq_finsuppProd_image`, `le_degree`, `le_weight`, `le_weight_of_ne_zero`, `le_weight_of_ne_zero'`, `nonTorsionWeight_of`, `nsmul_single_one_image`, `range_single_one`, `weight_apply`, `weight_eq_zero_iff_eq_zero`, `weight_single`, `weight_single_index`, `weight_single_one_apply`, `weight_sub_single_add`	30
Total	34

Finsupp

Definitions

Name	Category	Theorems
`NonTorsionWeight` 📖	CompData	1 math math: `nonTorsionWeight_of`
`degree` 📖	CompOp	38 math math: `finite_of_degree_le`, `degree_eq_sum`, `MvPolynomial.pow_idealOfVars`, `MvPolynomial.idealOfVars_eq_restrictSupportIdeal`, `MvPolynomial.mem_pow_idealOfVars_iff`, `MvPolynomial.coeff_homogeneousComponent`, `MvPolynomial.pow_idealOfVars_eq_span`, `MvPowerSeries.coeff_homogeneousComponent`, `degree_apply`, `le_degree`, `MvPolynomial.degree_degLexDegree`, `MvPolynomial.monomial_mem_pow_idealOfVars_iff`, `degree_eq_weight_one`, `degree_preimage_add`, `DegLex.lt_iff`, `MvPowerSeries.order_le`, `degLex_def`, `MvPowerSeries.exists_coeff_ne_zero_and_order`, `MvPolynomial.homogeneousComponent_apply`, `MvPowerSeries.totalDegree_trunc'`, `MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree`, `degree_preimage_nsmul`, `degree_single`, `MvPolynomial.homogeneousSubmodule_eq_finsupp_supported`, `range_single_one`, `MvPowerSeries.order_monomial`, `DegLex.le_iff`, `degree_eq_zero_iff`, `MvPowerSeries.order_eq_nat`, `MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree`, `degree_mono`, `DegLex.monotone_degree`, `nsmul_single_one_image`, `DegLex.lt_def`, `MvPowerSeries.order_monomial_of_ne_zero`, `degree_def`, `MvPolynomial.decomposition.decompose'_eq`, `image_pow_eq_finsuppProd_image`
`weight` 📖	CompOp	25 math math: `MvPowerSeries.weightedOrder_monomial`, `MvPolynomial.weightedDegree_eq_zero_iff`, `weight_single_one_apply`, `le_weight_of_ne_zero'`, `MvPolynomial.le_weightedTotalDegree`, `MvPowerSeries.weightedOrder_monomial_of_ne_zero`, `weight_single`, `MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported`, `finite_of_nat_weight_le`, `le_weight`, `degree_eq_weight_one`, `MvPowerSeries.le_weightedOrder_subst`, `weight_single_index`, `MvPowerSeries.coeff_weightedHomogeneousComponent`, `MvPowerSeries.weightedOrder_eq_nat`, `MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder`, `MvPowerSeries.weightedOrder_le`, `MvPolynomial.weightedDecomposition.decompose'_eq`, `le_weight_of_ne_zero`, `MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight`, `weight_sub_single_add`, `MvPolynomial.coeff_weightedHomogeneousComponent`, `weight_eq_zero_iff_eq_zero`, `weight_apply`, `MvPolynomial.weightedHomogeneousComponent_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_add` 📖	mathematical	—	`DFunLike.coe`	—	`map_add`
`degree_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Finset.sum` `support` `instFunLike`	—	—
`degree_def` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Finset.sum` `support` `instFunLike`	—	`degree_apply`
`degree_eq_sum` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Finset.sum` `Finset.univ` `instFunLike`	—	`degree_apply` `Finset.sum_subset`
`degree_eq_weight_one` 📖	mathematical	—	`degree` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `weight` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toModule`	—	`addHom_ext'` `AddMonoidHom.ext` `degree_single` `mul_one` `sum_single_index`
`degree_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `instZero`	—	`Unique.instSubsingleton`
`degree_mono` 📖	mathematical	—	`Monotone` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `preorder` `PartialOrder.toPreorder` `DFunLike.coe` `AddMonoidHom` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	—	`LE.le.trans` `Finset.sum_le_sum_of_subset` `support_mono` `Finset.sum_le_sum` `CanonicallyOrderedAdd.toAddLeftMono`
`degree_preimage_add` 📖	mathematical	—	`Set.preimage` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Set` `Set.add` `instAdd` `Nat.instAddMonoid`	—	`HasSubset.Subset.antisymm'` `Set.instAntisymmSubset` `Set.preimage_add_preimage_subset` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `exists_le_degree_eq` `le_iff_exists_add` `instCanonicallyOrderedAddOfAddLeftMono` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Set.add_mem_add` `map_add`
`degree_preimage_nsmul` 📖	mathematical	—	`Set.preimage` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Set` `Set.NSMul` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instZero` `instAdd` `Nat.instAddMonoid`	—	`zero_add` `one_smul` `succ_nsmul` `degree_preimage_add`
`degree_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `single`	—	`sum_single_index`
`degree_zero` 📖	mathematical	—	`DFunLike.coe`	—	`map_zero`
`exists_le_degree_eq` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	`MulZeroClass.toZero` `Nat.instMulZeroClass` `instLE`	—	`Nat.instCanonicallyOrderedAdd` `instCanonicallyOrderedAddOfAddLeftMono` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_iff_exists_add` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `map_zero` `AddMonoidHomClass.toZeroHomClass` `add_le_add_right` `isOrderedAddMonoid` `degree_single`
`finite_of_degree_le` 📖	mathematical	—	`Set.Finite` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	—	`degree_eq_weight_one` `finite_of_nat_weight_le`
`finite_of_nat_weight_le` 📖	mathematical	—	`Set.Finite` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `setOf` `DFunLike.coe` `AddMonoidHom` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule`	—	`Finset.coe_image` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `ext` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_imp_le_of_le_of_le` `le_weight` `le_refl` `Set.Finite.subset` `Finset.finite_toSet`
`image_pow_eq_finsuppProd_image` 📖	mathematical	—	`Set` `Set.NPow` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul` `Set.image` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `prod` `Monoid.toNatPow` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`prod_add_index` `pow_zero` `pow_add` `Set.image_pow` `MonoidHom.instMonoidHomClass` `Set.image_congr` `Set.image_comp` `Multiplicative.toAdd_image_nsmul` `Set.image_id` `Set.image_image` `prod_single_index` `pow_one`
`le_degree` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `AddMonoidHom` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	—	`Finset.single_le_sum_of_canonicallyOrdered`
`le_weight` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `instFunLike` `AddMonoidHom` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule`	—	`Finset.sum_congr` `Finset.sum_eq_add_sum_diff_singleton` `le_trans` `zero_le` `Nat.instCanonicallyOrderedAdd`
`le_weight_of_ne_zero` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `instAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule`	—	`Finset.sum_congr` `le_smul_of_one_le_left` `instSMulPosMonoNatOfIsOrderedAddMonoid` `Finset.sum_eq_add_sum_diff_singleton` `mem_support_iff` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Finset.sum_nonneg` `nsmul_nonneg`
`le_weight_of_ne_zero'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule`	—	`le_weight_of_ne_zero` `zero_le`
`nonTorsionWeight_of` 📖	mathematical	—	`NonTorsionWeight`	—	`smul_eq_zero` `IsDomain.toIsCancelMulZero`
`nsmul_single_one_image` 📖	mathematical	—	`Set` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Set.NSMul` `instZero` `instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Set.image` `single` `setOf` `DFunLike.coe` `AddMonoidHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `support`	—	`zero_nsmul` `Nat.instCanonicallyOrderedAdd` `Set.ext` `Finset.coe_empty` `succ_nsmul` `subset_antisymm` `Set.instAntisymmSubset` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `degree_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `le_iff_exists_add'` `instCanonicallyOrderedAddOfAddLeftMono` `Nat.instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `instIsEmptyFalse` `single_eq_same`
`range_single_one` 📖	mathematical	—	`Set.range` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `single` `setOf` `DFunLike.coe` `AddMonoidHom` `instAddZeroClass` `AddMonoidHom.instFunLike` `degree`	—	`subset_antisymm` `Set.instAntisymmSubset` `degree_single` `sum_eq_one_iff`
`weight_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `sum` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`weight_eq_zero_iff_eq_zero` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule` `AddZero.toZero` `Nat.instMulZeroClass` `instZero`	—	`ext` `NonTorsionWeight.ne_zero` `Nat.instNontrivial` `nonpos_iff_eq_zero` `le_weight_of_ne_zero'` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`weight_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `single` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`linearCombination_single`
`weight_single_index` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `Pi.single` `AddZero.toZero` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instFunLike`	—	`linearCombination_single_index`
`weight_single_one_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `weight` `Pi.single` `AddMonoidWithOne.toOne` `Semiring.toModule` `instFunLike`	—	`weight_single_index` `smul_eq_mul` `mul_one`
`weight_sub_single_add` 📖	mathematical	—	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Nat.instSemiring` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `weight` `AddCommMonoid.toNatModule` `Nat.instMulZeroClass` `tsub` `Nat.instAddCommMonoid` `Nat.instPartialOrder` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `single`	—	`Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `sub_add_single_one_cancel` `weight_apply` `sum_add_index'` `zero_smul` `add_smul` `sum_single_index` `one_smul`

Finsupp.NonTorsionWeight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_smul_eq_zero` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`ne_zero` 📖	—	—	—	—	`zero_ne_one` `NeZero.one` `eq_zero_of_smul_eq_zero` `one_smul`

LieModule

Definitions

Name	Category	Theorems
`Weight` 📖	CompData	87 math math: `LieAlgebra.IsKilling.rootSystem_toLinearMap_apply`, `LieAlgebra.IsKilling.iInf_ker_weight_eq_bot`, `Weight.IsZero.neg`, `LieAlgebra.IsKilling.restrict_killingForm_eq_sum`, `Weight.exists_ne_zero`, `traceForm_eq_sum_finrank_nsmul'`, `LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `LieAlgebra.IsKilling.rootSystem_coroot_apply`, `Weight.IsNonZero.neg`, `Weight.coe_zero`, `Weight.instFinite`, `LieAlgebra.IsKilling.corootSpace_eq_bot_iff`, `Weight.ext_iff`, `iSup_genWeightSpace_eq_top'`, `LieAlgebra.IsKilling.le_chainBotCoeff_of_rootSpace_ne_top`, `LieAlgebra.IsKilling.apply_coroot_eq_cast'`, `LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt`, `coe_chainTop`, `Weight.coe_coe`, `Weight.IsZero.eq`, `LieAlgebra.IsKilling.chainLength_zero`, `Weight.zero_apply`, `LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'`, `Weight.ext_iff'`, `LieAlgebra.cartan_sup_iSup_rootSpace_eq_top`, `LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `LieAlgebra.IsKilling.chainLength_neg`, `LieAlgebra.IsKilling.sl2SubmoduleOfRoot_eq_sup`, `Weight.coe_eq_zero_iff`, `LieAlgebra.IsKilling.coroot_mem_corootSpace`, `LieAlgebra.IsKilling.apply_coroot_eq_cast`, `genWeightSpace_chainBotCoeff_sub_one_zsmul_sub`, `LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem`, `Weight.isZero_neg`, `LieAlgebra.IsKilling.rootSpace_one_div_two_smul`, `LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing`, `Weight.coe_weight_mk`, `genWeightSpace_chainTopCoeff_add_one_zsmul_add`, `exists_forall_lie_eq_smul`, `LieAlgebra.IsKilling.biSup_corootSpace_eq_top`, `LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace`, `traceForm_eq_sum_finrank_nsmul`, `LieAlgebra.IsKilling.span_weight_isNonZero_eq_top`, `LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff`, `chainTopCoeff_add_one`, `LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff`, `LieAlgebra.IsKilling.root_apply_coroot`, `LieAlgebra.IsKilling.coroot_neg`, `LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan`, `coe_chainBot`, `Weight.apply_lie`, `LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace`, `LieAlgebra.IsKilling.rootSystem_pairing_apply`, `LieAlgebra.IsKilling.chainTopCoeff_zero_right`, `LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem`, `LieAlgebra.IsKilling.finrank_rootSpace_eq_one`, `LieAlgebra.IsKilling.chainLength_zero_right`, `LieAlgebra.IsKilling.chainBotCoeff_le_chainLength`, `LieAlgebra.IsKilling.traceForm_coroot`, `traceForm_eq_sum_finrank_nsmul_mul`, `LieAlgebra.IsKilling.coroot_zero`, `genWeightSpace_chainTopCoeff_add_one_nsmul_add`, `LieAlgebra.IsKilling.chainBotCoeff_zero_right`, `Weight.isNonZero_neg`, `Weight.isZero_zero`, `Weight.instIsEmptyOfSubsingleton`, `LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff`, `LieAlgebra.IsKilling.rootSpace_two_smul`, `Weight.apply_eq_zero_of_isNilpotent`, `chainTop_isNonZero`, `LieAlgebra.IsKilling.chainTopCoeff_le_chainLength`, `LieAlgebra.IsKilling.span_weight_eq_top`, `iSupIndep_genWeightSpace'`, `Weight.toLinear_neg`, `LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero`, `coe_chainTop'`, `range_traceForm_le_span_weight`, `genWeightSpace_neg_add_chainBot`, `genWeightSpace_add_chainTop`, `LieAlgebra.IsKilling.rootSystem_root_apply`, `Weight.coe_neg`, `Weight.instLinearMapClass`, `Weight.hasEigenvalueAt`, `LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton`, `Weight.toLinear_apply`, `LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple`, `Weight.isZero_iff_eq_zero`

---

← Back to Index