NoZeroDivisors

📁 Source: Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean

Statistics

Metric	Count
Definitions	0
Theorems X_mem_nonzeroDivisors, instNoZeroDivisors, mem_nonZeroDivisorsLeft_of_constantCoeff, mem_nonZeroDivisorsRight_of_constantCoeff, mem_nonZeroDivisors_of_constantCoeff, monomial_mem_nonzeroDivisors, monomial_mem_nonzeroDivisorsLeft, monomial_mem_nonzeroDivisorsRight, order_mul, order_prod, weightedOrder_mul, weightedOrder_prod	12
Total	12

MvPowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_mem_nonzeroDivisors 📖	mathematical	—	MvPowerSeries Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero instSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors X	—	X.eq_1 monomial_mem_nonzeroDivisors Submonoid.one_mem
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors MvPowerSeries instMul instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	WellOrderingRel.isWellOrder IsWellOrder.toIsWellFounded lexOrder_mul
mem_nonZeroDivisorsLeft_of_constantCoeff 📖	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisorsLeft DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff	—	—	ext WellFoundedLT.induction Finsupp.wellFoundedLT' Nat.instCanonicallyOrderedAdd instWellFoundedLTNat map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff Finset.sum_eq_single lt_of_le_of_ne Finset.HasAntidiagonal.mem_antidiagonal covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add IsOrderedCancelAddMonoid.toAddLeftReflectLT Finsupp.isOrderedCancelAddMonoid Nat.instIsOrderedCancelAddMonoid Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub MulZeroClass.mul_zero zero_add coeff_zero_eq_constantCoeff coeff_mul
mem_nonZeroDivisorsRight_of_constantCoeff 📖	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisorsRight DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff	—	—	ext WellFoundedLT.induction Finsupp.wellFoundedLT' Nat.instCanonicallyOrderedAdd instWellFoundedLTNat map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mul_right_mem_nonZeroDivisorsRight_eq_zero_iff Finset.sum_eq_single lt_of_le_of_ne Finset.HasAntidiagonal.mem_antidiagonal IsOrderedAddMonoid.toAddLeftMono Finsupp.isOrderedAddMonoid Nat.instIsOrderedAddMonoid Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finsupp.instCanonicallyOrderedAddOfAddLeftMono Nat.instOrderedSub Finsupp.instIsLeftCancelAdd MulZeroClass.zero_mul add_zero coeff_zero_eq_constantCoeff coeff_mul
mem_nonZeroDivisors_of_constantCoeff 📖	—	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe RingHom MvPowerSeries Semiring.toNonAssocSemiring instSemiring RingHom.instFunLike constantCoeff	—	—	mem_nonZeroDivisorsLeft_of_constantCoeff mem_nonZeroDivisorsRight_of_constantCoeff
monomial_mem_nonzeroDivisors 📖	mathematical	—	MvPowerSeries Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero instSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial	—	Iff.and monomial_mem_nonzeroDivisorsLeft monomial_mem_nonzeroDivisorsRight
monomial_mem_nonzeroDivisorsLeft 📖	mathematical	—	MvPowerSeries Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero instSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisorsLeft DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial	—	monomial_zero_eq_C monomial_mul_monomial ext add_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_tsub_cancel_right Finsupp.orderedSub Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_add_self Finsupp.instCanonicallyOrderedAddOfAddLeftMono coeff_monomial_mul
monomial_mem_nonzeroDivisorsRight 📖	mathematical	—	MvPowerSeries Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero instSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisorsRight DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid Semiring.toModule instModule LinearMap.instFunLike monomial	—	monomial_zero_eq_C monomial_mul_monomial ext zero_add map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_tsub_cancel_right Finsupp.orderedSub Finsupp.addLeftReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_add_self Finsupp.instCanonicallyOrderedAddOfAddLeftMono coeff_mul_monomial
order_mul 📖	mathematical	—	order MvPowerSeries instMul ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	weightedOrder_mul
order_prod 📖	mathematical	—	order CommSemiring.toSemiring Finset.prod MvPowerSeries CommSemiring.toCommMonoid instCommSemiring Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	weightedOrder_prod
weightedOrder_mul 📖	mathematical	—	weightedOrder MvPowerSeries instMul ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_antisymm instNoZeroDivisors weightedHomogeneousComponent_of_weightedOrder ne_zero_iff_weightedOrder_finite ENat.coe_toNat ne_top_of_lt Nat.cast_add not_lt weightedHomogeneousComponent_mul_of_le_weightedOrder le_of_eq weightedHomogeneousComponent_of_lt_weightedOrder_eq_zero not_lt_top_iff add_top top_add le_weightedOrder_mul
weightedOrder_prod 📖	mathematical	—	weightedOrder CommSemiring.toSemiring Finset.prod MvPowerSeries CommSemiring.toCommMonoid instCommSemiring Finset.sum ENat LinearOrderedAddCommMonoidWithTop.toAddCommMonoid instLinearOrderedAddCommMonoidWithTopENat	—	Finset.cons_induction weightedOrder_one Finset.sum_cons Finset.prod_cons weightedOrder_mul

---

← Back to Index