Ideal

📁 Source: Mathlib/RingTheory/UniqueFactorizationDomain/Ideal.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_mem_prime_of_ne_bot, setOf_isPrincipal_wellFoundedOn_gt, of_setOf_isPrincipal_wellFoundedOn_gt	3
Total	3

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
setOf_isPrincipal_wellFoundedOn_gt 📖	mathematical	—	Set.WellFoundedOn Ideal CommSemiring.toSemiring setOf Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	Set.ext Set.image_univ Set.wellFoundedOn_image Set.wellFoundedOn_univ span_singleton_lt_span_singleton wellFounded_dvdNotUnit

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_prime_of_ne_bot 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Prime CommSemiring.toCommMonoidWithZero	—	Submodule.exists_mem_ne_zero_of_ne_bot UniqueFactorizationMonoid.factors_prod Ideal.mul_unit_mem_iff_mem Units.isUnit multiset_prod_mem_iff_exists_mem UniqueFactorizationMonoid.prime_of_factor

WfDvdMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_setOf_isPrincipal_wellFoundedOn_gt 📖	mathematical	Set.WellFoundedOn Ideal CommSemiring.toSemiring setOf Submodule.IsPrincipal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	WfDvdMonoid CommSemiring.toCommMonoidWithZero	—	Ideal.span_singleton_lt_span_singleton

---

← Back to Index