PrincipalIdealDomainOfPrime

📁 Source: Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

Statistics

Metric	Count
Definitions	0
Theorems isOka_isPrincipal, of_prime, of_prime_ne_bot	3
Total	3

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOka_isPrincipal 📖	mathematical	—	IsOka Submodule.IsPrincipal CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	top_isPrincipal le_antisymm submodule_span_eq mem_sup_left mem_sup_right mem_span_singleton_self mem_span_singleton' mem_colon_span_singleton mul_comm mul_assoc mul_mem_right instIsTwoSided IsScalarTower.left span_singleton_mul_span_singleton sup_mul sup_le_iff span_singleton_le_iff_mem mul_le_right

IsPrincipalIdealRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_prime 📖	mathematical	Submodule.IsPrincipal CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	IsPrincipalIdealRing	—	Ideal.IsOka.forall_of_forall_prime Ideal.isOka_isPrincipal Ideal.exists_maximal_not_isPrincipal isPrincipalIdealRing_iff
of_prime_ne_bot 📖	mathematical	Submodule.IsPrincipal CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	IsPrincipalIdealRing	—	of_prime eq_or_ne bot_isPrincipal

---

← Back to Index