Ideal

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

Statistics

Metric	Count
Definitions	0
Theorems mem_ideal_span_of'_image, mem_ideal_span_of_image	2
Total	2

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ideal_span_of'_image 📖	mathematical	—	AddMonoidAlgebra Ideal semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set.image of' Set Set.instMembership AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	MonoidAlgebra.mem_ideal_span_of_image

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_ideal_span_of_image 📖	mathematical	—	MonoidAlgebra Ideal semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set.image DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring MonoidHom.instFunLike of Set Set.instMembership MulOne.toMul	—	Finset.mem_union Finsupp.support_add instIsEmptyFalse Finset.mem_biUnion Finsupp.support_sum mul_def mul_assoc Finset.mem_singleton Finsupp.support_single_subset Ideal.span_le one_mul Finsupp.sum_single Ideal.sum_mem Set.image_congr single_mul_single mul_one Ideal.mul_mem_left Ideal.subset_span Set.mem_image_of_mem

---

← Back to Index