Oka

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

Statistics

Metric	Count
Definitions IsOka	1
Theorems forall_of_forall_prime, forall_of_forall_prime', isPrime_of_maximal_not, oka, top	5
Total	6

Ideal

Definitions

Name	Category	Theorems
IsOka 📖	CompData	2 math math: isOka_fg, isOka_isPrincipal

Ideal.IsOka

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_of_forall_prime 📖	—	Ideal.IsOka Maximal Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—	Maximal.prop isPrime_of_maximal_not
forall_of_forall_prime' 📖	—	Ideal.IsOka Ideal CommSemiring.toSemiring Set Set.instMembership	—	—	forall_of_forall_prime zorn_le_nonempty₀ le_sSup
isPrime_of_maximal_not 📖	mathematical	Ideal.IsOka Maximal Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal.IsPrime	—	Maximal.prop top Mathlib.Tactic.Push.not_forall_eq of_not_not Maximal.not_prop_of_gt Submodule.lt_sup_iff_notMem lt_of_le_of_ne Ideal.le_colon Ideal.instIsTwoSided Ideal.mem_colon_span_singleton mul_comm oka
oka 📖	—	Ideal.IsOka Ideal CommSemiring.toSemiring SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Ideal.span Set Set.instSingletonSet Submodule.colon NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.coe Submodule.setLike	—	—	—
top 📖	mathematical	Ideal.IsOka	Top.top Ideal CommSemiring.toSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—

---

← Back to Index