Semiring

📁 Source: Mathlib/Data/Set/Semiring.lean

Statistics

Metric	Count
Definitions Semiring, up, down, imageHom, instAdd, instAddCommMonoid, instCommMonoid, instIdemCommSemiringOfCommMonoid, instIdemSemiringOfMonoid, instNonAssocSemiringOfMulOneClass, instNonUnitalCommSemiringOfCommSemigroup, instNonUnitalNonAssocSemiring, instNonUnitalSemiringOfSemigroup, instOne, instZero, singletonMonoidHom, instInhabitedSetSemiring, instOrderBotSetSemiring, instPartialOrderSetSemiring	19
Theorems up_empty, up_image, up_mul, up_one, up_union, addLeftMono, add_def, down_add, down_imageHom, down_mul, down_one, down_ssubset_down, down_subset_down, down_up, down_zero, imageHom_def, instCanonicallyOrderedAdd, instIsOrderedRing, instNoZeroDivisors, mulLeftMono, mulRightMono, mul_def, one_def, up_down, up_le_up, up_lt_up, zero_def	27
Total	46

Set

Definitions

Name	Category	Theorems
up 📖	CompOp	15 math math: up_union, SetSemiring.up_lt_up, SetSemiring.imageHom_def, SetSemiring.zero_def, up_mul, SetSemiring.add_def, up_empty, SetSemiring.one_def, Submodule.singleton_smul, up_image, SetSemiring.up_le_up, up_one, SetSemiring.down_up, SetSemiring.mul_def, SetSemiring.up_down

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
up_empty 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike up instEmptyCollection SetSemiring.instZero	—	—
up_image 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike up image MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike RingHom SetSemiring.instNonAssocSemiringOfMulOneClass RingHom.instFunLike SetSemiring.imageHom	—	—
up_mul 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike up mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SetSemiring.instNonUnitalNonAssocSemiring	—	—
up_one 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike up one SetSemiring.instOne	—	—
up_union 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike up instUnion SetSemiring.instAdd	—	—

SetSemiring

Definitions

Name	Category	Theorems
down 📖	CompOp	14 math math: imageHom_def, down_one, down_mul, add_def, down_imageHom, down_add, down_ssubset_down, down_subset_down, Submodule.setSemiring_smul_def, down_up, Submodule.span.ringHom_apply, mul_def, down_zero, up_down
imageHom 📖	CompOp	3 math math: imageHom_def, Set.up_image, down_imageHom
instAdd 📖	CompOp	5 math math: Set.up_union, instCanonicallyOrderedAdd, add_def, down_add, addLeftMono
instAddCommMonoid 📖	CompOp	—
instCommMonoid 📖	CompOp	—
instIdemCommSemiringOfCommMonoid 📖	CompOp	—
instIdemSemiringOfMonoid 📖	CompOp	4 math math: instIsOrderedRing, Submodule.smul_le_smul, Submodule.singleton_smul, Submodule.setSemiring_smul_def
instNonAssocSemiringOfMulOneClass 📖	CompOp	4 math math: imageHom_def, Set.up_image, down_imageHom, Submodule.span.ringHom_apply
instNonUnitalCommSemiringOfCommSemigroup 📖	CompOp	—
instNonUnitalNonAssocSemiring 📖	CompOp	6 math math: mulRightMono, down_mul, mulLeftMono, Set.up_mul, mul_def, instNoZeroDivisors
instNonUnitalSemiringOfSemigroup 📖	CompOp	—
instOne 📖	CompOp	3 math math: down_one, one_def, Set.up_one
instZero 📖	CompOp	4 math math: zero_def, Set.up_empty, instNoZeroDivisors, down_zero
singletonMonoidHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addLeftMono 📖	mathematical	—	AddLeftMono SetSemiring instAdd Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring	—	Set.union_subset_union_right
add_def 📖	mathematical	—	SetSemiring instAdd DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.instUnion down	—	—
down_add 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down instAdd Set.instUnion	—	—
down_imageHom 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down RingHom instNonAssocSemiringOfMulOneClass RingHom.instFunLike imageHom Set.image MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike	—	—
down_mul 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instNonUnitalNonAssocSemiring Set.mul	—	—
down_one 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down instOne Set.one	—	—
down_ssubset_down 📖	mathematical	—	Set Set.instHasSSubset DFunLike.coe Equiv SetSemiring EquivLike.toFunLike Equiv.instEquivLike down Preorder.toLT PartialOrder.toPreorder instPartialOrderSetSemiring	—	—
down_subset_down 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe Equiv SetSemiring EquivLike.toFunLike Equiv.instEquivLike down Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring	—	—
down_up 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down Set.up	—	—
down_zero 📖	mathematical	—	DFunLike.coe Equiv SetSemiring Set EquivLike.toFunLike Equiv.instEquivLike down instZero Set.instEmptyCollection	—	—
imageHom_def 📖	mathematical	—	DFunLike.coe RingHom SetSemiring instNonAssocSemiringOfMulOneClass RingHom.instFunLike imageHom Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.image MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike down	—	—
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd SetSemiring instAdd Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring	—	Set.union_eq_right Set.subset_union_right Set.subset_union_left
instIsOrderedRing 📖	mathematical	—	IsOrderedRing SetSemiring IdemSemiring.toSemiring instIdemSemiringOfMonoid CommMonoid.toMonoid instPartialOrderSetSemiring	—	CanonicallyOrderedAdd.toIsOrderedRing instCanonicallyOrderedAdd
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors SetSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instNonUnitalNonAssocSemiring instZero	—	Set.eq_empty_or_nonempty Set.Nonempty.ne_empty Set.mul_mem_mul Set.Nonempty.some_mem
mulLeftMono 📖	mathematical	—	MulLeftMono SetSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instNonUnitalNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring	—	Set.mul_subset_mul_left
mulRightMono 📖	mathematical	—	MulRightMono SetSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instNonUnitalNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring	—	Set.mul_subset_mul_right
mul_def 📖	mathematical	—	SetSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instNonUnitalNonAssocSemiring DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.mul down	—	—
one_def 📖	mathematical	—	SetSemiring instOne DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.one	—	—
up_down 📖	mathematical	—	DFunLike.coe Equiv Set SetSemiring EquivLike.toFunLike Equiv.instEquivLike Set.up down	—	—
up_le_up 📖	mathematical	—	SetSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrderSetSemiring DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.instHasSubset	—	—
up_lt_up 📖	mathematical	—	SetSemiring Preorder.toLT PartialOrder.toPreorder instPartialOrderSetSemiring DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.instHasSSubset	—	—
zero_def 📖	mathematical	—	SetSemiring instZero DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.instEmptyCollection	—	—

(root)

Definitions

Name	Category	Theorems
Semiring 📖	CompData	5 math math: Ring.toSemiring_injective, Semiring.toNonUnitalSemiring_injective, nonempty_semiring_iff, CommSemiring.toSemiring_injective, Semiring.toNonAssocSemiring_injective
instInhabitedSetSemiring 📖	CompOp	—
instOrderBotSetSemiring 📖	CompOp	—
instPartialOrderSetSemiring 📖	CompOp	9 math math: SetSemiring.instIsOrderedRing, SetSemiring.mulRightMono, SetSemiring.up_lt_up, SetSemiring.mulLeftMono, SetSemiring.instCanonicallyOrderedAdd, SetSemiring.up_le_up, SetSemiring.down_ssubset_down, SetSemiring.down_subset_down, SetSemiring.addLeftMono

---

← Back to Index