Ideal

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

Statistics

Metric	Count
Definitions	0
Theorems eq_of_le_of_X_notMem_of_fg_of_isPrime, eq_span_insert_X_of_X_mem_of_span_eq, exist_eq_span_eq_ncard_of_X_notMem, fg_iff_of_isPrime, instIsNoetherianRing, instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain, map_constantCoeff_le_self_of_X_mem, spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime, spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem, spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime	10
Total	10

PowerSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_le_of_X_notMem_of_fg_of_isPrime 📖	—	Ideal PowerSeries instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike X Ideal.FG Ideal.map RingHom RingHom.instFunLike constantCoeff	—	—	LE.le.antisymm' LE.le.antisymm Ideal.map_mono Submodule.fg_iff_exists_fin_generating_family map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_sum Finset.sum_congr map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass sub_self map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass sub_zero DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass coeff_C_mul sub_const_eq_X_mul_shift Ideal.IsPrime.mul_mem_iff_mem_or_mem Ideal.instIsTwoSided_1 Ideal.sub_mem Ideal.sum_mem Ideal.mul_mem_left Ideal.subset_span Set.mem_range_self MulZeroClass.zero_mul Finset.sum_const_zero pow_zero one_mul trunc_succ Polynomial.coe_add Polynomial.coe_monomial monomial_eq_C_mul_X_pow add_mul Distrib.rightDistribClass mul_assoc mul_left_comm Finset.sum_add_distrib pow_succ mul_sub Finset.mul_sum ext trunc_sub trunc_trunc_mul Polynomial.coeff_sub coeff_trunc IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass Polynomial.finset_sum_coeff trunc_X_pow_self_mul Zero.instNonempty Ideal.mem_span_range_iff_exists_fun Eq.le Set.range_comp Ideal.map_span Ideal.submodule_span_eq Ideal.mem_map_of_mem Function.sometimes_spec
eq_span_insert_X_of_X_mem_of_span_eq 📖	mathematical	PowerSeries Ideal instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule X Ideal.span Ideal.map RingHom RingHom.instFunLike constantCoeff	Set Set.instInsert Set.image DFunLike.coe C	—	Ideal.span_insert Ideal.map_span RingHom.instRingHomClass Ideal.map_map le_antisymm Ideal.mem_span_singleton_sup Ideal.mem_map_of_mem eq_shift_mul_X_add_const
exist_eq_span_eq_ncard_of_X_notMem 📖	mathematical	PowerSeries Ideal instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule X Ideal.span Ideal.map RingHom RingHom.instFunLike constantCoeff	Set.Finite Set.ncard	—	Ideal.mem_map_iff_of_surjective RingHom.instRingHomClass constantCoeff_surj Ideal.subset_span Set.SurjOn.exists_subset_injOn_image_eq eq_of_le_of_X_notMem_of_fg_of_isPrime Ideal.span_le Submodule.fg_def Set.Finite.of_finite_image Ideal.map_le_iff_le_comap Ideal.mem_comap Ideal.mem_map_of_mem Submodule.span_induction ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Ideal.add_mem map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Submodule.smul_of_tower_mem IsScalarTower.right Set.Finite.of_injOn Set.mem_image_of_mem Set.InjOn.ncard_image
fg_iff_of_isPrime 📖	mathematical	—	Ideal.FG PowerSeries instSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike constantCoeff	—	Ideal.FG.map eq_span_insert_X_of_X_mem_of_span_eq Set.Finite.insert Set.Finite.image Finset.finite_toSet CanLift.prf Set.instCanLiftFinsetCoeFinite exist_eq_span_eq_ncard_of_X_notMem
instIsNoetherianRing 📖	mathematical	—	IsNoetherianRing PowerSeries instSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsNoetherianRing.of_prime fg_iff_of_isPrime isNoetherianRing_iff_ideal_fg
instUniqueFactorizationMonoidOfIsPrincipalIdealRingOfIsDomain 📖	mathematical	—	UniqueFactorizationMonoid PowerSeries CommSemiring.toCommMonoidWithZero instCommSemiring CommRing.toCommSemiring	—	UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime instIsDomain X_prime Submodule.IsPrincipal.principal IsPrincipalIdealRing.principal exist_eq_span_eq_ncard_of_X_notMem Set.finite_singleton Set.ncard_singleton Ideal.mem_span_singleton_self Ideal.span_singleton_prime Iff.not Ideal.span_singleton_eq_bot
map_constantCoeff_le_self_of_X_mem 📖	mathematical	PowerSeries Ideal instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule X	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal.map RingHom RingHom.instFunLike RingHom.comp C constantCoeff	—	sub_eq_iff_eq_add' eq_X_mul_shift_add_const sub_mem Submodule.addSubgroupClass Ideal.mul_mem_right Ideal.instIsTwoSided_1 RingHom.instRingHomClass
spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime 📖	mathematical	PowerSeries Ideal instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule X Ideal.FG	Submodule.spanFinrank Ideal.map RingHom RingHom.instFunLike constantCoeff	—	le_antisymm constantCoeff_surj exist_eq_span_eq_ncard_of_X_notMem Submodule.span_generators Submodule.FG.finite_generators Submodule.FG.map Ideal.map_eq_submodule_map le_trans Submodule.spanFinrank_span_le_ncard_of_finite Submodule.FG.generators_ncard le_refl Ideal.spanFinrank_map_le_of_fg
spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem 📖	mathematical	PowerSeries Ideal instSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule X	Submodule.spanFinrank Ideal.map RingHom RingHom.instFunLike constantCoeff	—	constantCoeff_surj Submodule.FG.map Ideal.map_eq_submodule_map eq_span_insert_X_of_X_mem_of_span_eq Submodule.span_generators le_trans Submodule.spanFinrank_span_le_ncard_of_finite Set.Finite.map Submodule.FG.finite_generators Set.ncard_insert_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Set.ncard_image_le Submodule.FG.generators_ncard le_refl Submodule.spanFinrank_of_not_fg
spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime 📖	mathematical	—	Submodule.spanFinrank PowerSeries instSemiring CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike constantCoeff	—	spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem le_trans Eq.le spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime Submodule.spanFinrank_of_not_fg

---

← Back to Index