OfPrime

📁 Source: Mathlib/RingTheory/Noetherian/OfPrime.lean

Statistics

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

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOka_fg 📖	mathematical	—	IsOka CommRing.toCommSemiring FG CommSemiring.toSemiring	—	Finset.coe_singleton span_singleton_one Submodule.fg_iff_exists_fin_generating_family mem_span_singleton_sup sup_comm submodule_span_eq mem_span_range_self le_antisymm Finset.coe_union Finset.coe_image Finset.coe_univ Set.image_univ Set.image_congr span_union mem_colon_span_singleton mul_comm Submodule.mem_sup mem_span_range_iff_exists_fun mem_sup_left sum_mem mul_mem_left smul_eq_mul Set.range_smul Algebra.to_smulCommClass Submodule.span_smul Set.smul_mem_smul_set add_mem_iff_right add_comm Finset.sum_mul Finset.sum_add_distrib Finset.sum_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_prime 📖	mathematical	Ideal.FG CommSemiring.toSemiring CommRing.toCommSemiring	IsNoetherianRing	—	Ideal.IsOka.forall_of_forall_prime' Ideal.isOka_fg DirectedOn.exists_mem_subset_of_finset_subset_biUnion IsChain.directedOn instReflLe Submodule.mem_sSup_of_directed Ideal.subset_span le_antisymm le_sSup Ideal.span_le
of_prime_ne_bot 📖	mathematical	Ideal.FG CommSemiring.toSemiring CommRing.toCommSemiring	IsNoetherianRing	—	of_prime eq_or_ne Submodule.fg_bot

---

← Back to Index