Colon

📁 Source: Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_eq_colon_of_mem_minimalPrimes	1
Total	1

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_colon_of_mem_minimalPrimes 📖	—	Ideal CommSemiring.toSemiring Set Set.instMembership Ideal.minimalPrimes colon Set.instSingletonSet	—	—	Ideal.minimalPrimes_top IsScalarTower.right Ideal.exists_radical_pow_le_of_fg Ideal.fg_of_isNoetherianRing Mathlib.Tactic.Contrapose.contrapose₃ pow_zero Ideal.one_eq_top Ideal.finite_minimalPrimes_of_isNoetherianRing IsScalarTower.left mul_pow le_imp_le_of_le_of_le pow_le_pow_left₀ IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono mul_nonneg zero_le instCanonicallyOrderedAdd Ideal.mul_le_inf Ideal.instIsTwoSided le_refl Finset.inf_insert Finset.insert_erase Set.Finite.mem_toFinset Finset.inf_id_eq_sInf Set.Finite.coe_toFinset Ideal.sInf_minimalPrimes le_antisymm Ideal.IsPrime.pow_le_iff Ideal.IsPrime.inf_le' Nat.find_spec mem_colon_singleton smul_smul mul_pow_sub_one mul_mem_mul Module.Finite.fg_top Module.instFiniteSubtypeMemIdealOfIsNoetherian Ideal.IsPrime.prod_mem_iff RingHomSurjective.ids map_subtype_top map_injective_of_injective subtype_injective map_span span_le Set.image_subset_iff Set.mem_preimage SetLike.mem_coe SMulCommClass.smul_comm smulCommClass_self Finset.dvd_prod_of_mem Ideal.mul_mem_right mul_comm Ideal.span_singleton_mul_le_iff SemigroupAction.mul_smul mul_assoc Ideal.IsPrime.mul_le Ideal.span_singleton_le_iff_mem LE.le.trans tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Ideal.top_mul instIsConcreteLE

---

← Back to Index