Kaplansky

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

Statistics

Metric	Count
Definitions	0
Theorems iff_exists_prime_mem_of_isPrime	1
Total	1

UniqueFactorizationMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_exists_prime_mem_of_isPrime 📖	mathematical	—	UniqueFactorizationMonoid CommSemiring.toCommMonoidWithZero Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Prime	—	Ideal.IsPrime.exists_mem_prime_of_ne_bot

---

← Back to Index