Ideal

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

Statistics

Metric	Count
Definitions	0
Theorems map, mul, pow, exists_pow_le_of_le_radical_of_fg, exists_pow_le_of_le_radical_of_fg_radical, exists_radical_pow_le_of_fg, fg_ker_comp, smul	8
Total	8

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pow_le_of_le_radical_of_fg 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule radical FG	Submodule.instPowNat IsScalarTower.right Algebra.id	—	Submodule.fg_induction IsScalarTower.right span_singleton_pow instIsTwoSided LE.le.trans le_sup_left le_sup_right sup_pow_add_le_pow_sup_pow sup_le
exists_pow_le_of_le_radical_of_fg_radical 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule radical FG	Submodule.instPowNat IsScalarTower.right Algebra.id	—	IsScalarTower.right exists_radical_pow_le_of_fg LE.le.trans IsScalarTower.left pow_right_mono
exists_radical_pow_le_of_fg 📖	mathematical	FG CommSemiring.toSemiring radical	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	—	le_refl Submodule.fg_induction IsScalarTower.right subset_span Set.mem_singleton span.eq_1 IsScalarTower.left span_singleton_pow instIsTwoSided span_le Set.singleton_subset_iff mem_sup_left mem_sup_right add_eq_sup add_pow sum_eq_sup Finset.sup_le_iff LE.le.trans mul_le_right le_or_gt pow_le_pow_right mul_le_left
fg_ker_comp 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass DFunLike.coe	RingHom.comp	—	RingHom.instRingHomClass IsScalarTower.of_algebraMap_eq Submodule.fg_ker_comp Submodule.FG.restrictScalars_of_surjective IsScalarTower.right

Ideal.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Ideal.FG	Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Finset.coe_image Ideal.map_span RingHom.instRingHomClass
mul 📖	mathematical	Ideal.FG	Ideal Submodule.mul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction	—	Submodule.FG.smul
pow 📖	mathematical	Ideal.FG	Ideal Submodule.instPowNat Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction	—	IsScalarTower.left Submodule.pow_zero Ideal.one_eq_top Ideal.fg_top Ideal.IsTwoSided.pow_succ mul

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul 📖	mathematical	Ideal.FG Submodule.FG	Ideal Submodule Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left Submodule.span_smul_span Finset.coe_smul

---

← Back to Index