Radical

📁 Source: Mathlib/RingTheory/GradedAlgebra/Radical.lean

Statistics

Metric	Count
Definitions radical	1
Theorems coe_radical, isPrime_iff, isPrime_of_homogeneous_mem_or_mem, radical, radical_eq, homogeneousCore	6
Total	7

HomogeneousIdeal

Definitions

Name	Category	Theorems
radical 📖	CompOp	1 math math: coe_radical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_radical 📖	mathematical	—	toIdeal Ring.toSemiring CommRing.toRing LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid radical Ideal.radical CommRing.toCommSemiring	—	—

Ideal.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPrime_iff 📖	mathematical	Ideal.IsHomogeneous CommSemiring.toSemiring CommRing.toCommSemiring LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid	Ideal.IsPrime Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.IsPrime.ne_top Ideal.IsPrime.mem_or_mem isPrime_of_homogeneous_mem_or_mem
isPrime_of_homogeneous_mem_or_mem 📖	mathematical	Ideal.IsHomogeneous CommSemiring.toSemiring CommRing.toCommSemiring LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal.IsPrime	—	Finset.filter_nonempty_iff Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq AddSubmonoidClass.toZeroMemClass DirectSum.sum_support_decompose Ideal.sum_mem Finset.max'_mem Finset.mem_of_mem_filter Finset.sum_congr SetLike.GradedMonoid.toGradedMul GradedRing.toGradedMonoid DirectSum.decompose_mul DirectSum.coe_mul_apply Finset.add_sum_erase eq_sub_of_add_eq Ideal.sub_mem Ne.le_iff_lt add_left_cancel IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd le_or_lt_of_add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono IsCancelAdd.toIsRightCancelAdd covariant_swap_add_of_covariant_add Eq.ge lt_irrefl Finset.max'_lt_iff Ideal.mul_mem_right Ideal.instIsTwoSided_1 Ideal.mul_mem_left Finset.mem_filter SetLike.coe_mem
radical 📖	mathematical	Ideal.IsHomogeneous CommSemiring.toSemiring CommRing.toCommSemiring LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid	Ideal.radical	—	radical_eq sInf
radical_eq 📖	mathematical	Ideal.IsHomogeneous CommSemiring.toSemiring CommRing.toCommSemiring LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid	Ideal.radical InfSet.sInf Ideal Ring.toSemiring CommRing.toRing Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule setOf Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal.IsPrime	—	Ideal.radical_eq_sInf le_antisymm sInf_le_sInf sInf_le_sInf_of_isCoinitialFor HomogeneousIdeal.isHomogeneous Eq.trans_le toIdeal_homogeneousCore_eq_self Ideal.homogeneousCore_mono Ideal.IsPrime.homogeneousCore Ideal.toIdeal_homogeneousCore_le

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homogeneousCore 📖	mathematical	—	Ideal.IsPrime CommSemiring.toSemiring CommRing.toCommSemiring HomogeneousIdeal.toIdeal LinearOrder.toDecidableEq AddCommMonoid.toAddMonoid Ideal.homogeneousCore	—	Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem HomogeneousIdeal.isHomogeneous ne_top_of_le_ne_top ne_top Ideal.toIdeal_homogeneousCore_le mem_or_mem Ideal.mem_homogeneousCore_of_homogeneous_of_mem

---

← Back to Index