NoZeroDivisors

📁 Source: Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsCancelAddZeroOfIsCancelAddOfUniqueSums, instIsDomainOfIsCancelAddOfUniqueSums, instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums, instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums, instNoZeroDivisorsOfUniqueSums, mul_apply_add_eq_mul_of_uniqueAdd, instIsCancelMulZeroOfIsCancelAddOfUniqueProds, instIsDomainOfIsCancelAddOfUniqueProds, instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds, instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds, instNoZeroDivisorsOfUniqueProds, mul_apply_mul_eq_mul_of_uniqueMul	12
Total	12

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCancelAddZeroOfIsCancelAddOfUniqueSums 📖	mathematical	—	IsCancelMulZero AddMonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums IsCancelMulZero.toIsLeftCancelMulZero instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums IsCancelMulZero.toIsRightCancelMulZero
instIsDomainOfIsCancelAddOfUniqueSums 📖	mathematical	—	IsDomain AddMonoidAlgebra semiring	—	instIsCancelAddZeroOfIsCancelAddOfUniqueSums IsDomain.toIsCancelMulZero nontrivial IsDomain.toNontrivial Zero.instNonempty
instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums 📖	mathematical	—	IsLeftCancelMulZero AddMonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	Finset.eraseInduction Finset.eq_empty_or_nonempty Finsupp.support_eq_empty Finset.union_eq_empty UniqueSums.uniqueAdd_of_nonempty Finsupp.support_nonempty_iff mul_apply_add_eq_mul_of_uniqueAdd UniqueAdd.mono subset_rfl Finset.instReflSubset Finset.subset_union_left mul_left_cancel₀ Finsupp.mem_support_iff Finset.subset_union_right Finsupp.erase_add_single add_right_cancel_iff IsCancelAdd.toIsRightCancelAdd instIsCancelAdd mul_add Distrib.leftDistribClass Finsupp.support_erase Finset.erase_union_distrib
instIsRightCancelAddZeroOfIsCancelAddOfUniqueSums 📖	mathematical	—	IsRightCancelMulZero AddMonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	MulOpposite.isLeftCancelMulZero_iff Function.Injective.isLeftCancelMulZero RingEquiv.injective map_zero AddMonoidHomClass.toZeroHomClass NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.instRingEquivClass map_mul NonUnitalRingHomClass.toMulHomClass instIsLeftCancelAddZeroOfIsCancelAddOfUniqueSums MulOpposite.instIsCancelAdd MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero UniqueSums.instAddOpposite
instNoZeroDivisorsOfUniqueSums 📖	mathematical	—	NoZeroDivisors AddMonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	Mathlib.Tactic.Contrapose.contrapose₁ UniqueSums.uniqueAdd_of_nonempty Finsupp.support_nonempty_iff Finsupp.mem_support_iff mul_ne_zero mul_apply_add_eq_mul_of_uniqueAdd
mul_apply_add_eq_mul_of_uniqueAdd 📖	mathematical	UniqueAdd Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFunLike.coe Finsupp Finsupp.instFunLike AddMonoidAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_apply Finset.sum_congr Finset.sum_product' Finset.sum_eq_single Finset.mem_product not_and_or Finsupp.notMem_support_iff MulZeroClass.zero_mul MulZeroClass.mul_zero

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCancelMulZeroOfIsCancelAddOfUniqueProds 📖	mathematical	—	IsCancelMulZero MonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds IsCancelMulZero.toIsLeftCancelMulZero instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds IsCancelMulZero.toIsRightCancelMulZero
instIsDomainOfIsCancelAddOfUniqueProds 📖	mathematical	—	IsDomain MonoidAlgebra semiring	—	instIsCancelMulZeroOfIsCancelAddOfUniqueProds IsDomain.toIsCancelMulZero nontrivial IsDomain.toNontrivial One.instNonempty
instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds 📖	mathematical	—	IsLeftCancelMulZero MonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	Finset.eraseInduction Finset.eq_empty_or_nonempty UniqueProds.uniqueMul_of_nonempty Finsupp.support_nonempty_iff mul_apply_mul_eq_mul_of_uniqueMul UniqueMul.mono subset_rfl Finset.instReflSubset Finset.subset_union_left mul_left_cancel₀ Finsupp.mem_support_iff Finset.subset_union_right Finsupp.erase_add_single IsCancelAdd.toIsRightCancelAdd instIsCancelAdd mul_add Distrib.leftDistribClass Finsupp.support_erase Finset.erase_union_distrib
instIsRightCancelMulZeroOfIsCancelAddOfUniqueProds 📖	mathematical	—	IsRightCancelMulZero MonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	MulOpposite.isLeftCancelMulZero_iff Function.Injective.isLeftCancelMulZero RingEquiv.injective map_zero AddMonoidHomClass.toZeroHomClass NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass RingEquiv.instRingEquivClass map_mul NonUnitalRingHomClass.toMulHomClass instIsLeftCancelMulZeroOfIsCancelAddOfUniqueProds MulOpposite.instIsCancelAdd MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero UniqueProds.instMulOpposite
instNoZeroDivisorsOfUniqueProds 📖	mathematical	—	NoZeroDivisors MonoidAlgebra instMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass nonUnitalNonAssocSemiring	—	Mathlib.Tactic.Contrapose.contrapose₁ UniqueProds.uniqueMul_of_nonempty Finsupp.support_nonempty_iff Finsupp.mem_support_iff mul_ne_zero mul_apply_mul_eq_mul_of_uniqueMul
mul_apply_mul_eq_mul_of_uniqueMul 📖	mathematical	UniqueMul Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFunLike.coe Finsupp Finsupp.instFunLike MonoidAlgebra instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_apply Finset.sum_congr Finset.sum_eq_single not_and_or Finsupp.notMem_support_iff MulZeroClass.zero_mul MulZeroClass.mul_zero

---

← Back to Index