Nakayama

📁 Source: Mathlib/RingTheory/Nakayama.lean

Statistics

Metric	Count
Definitions	0
Theorems eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator, eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator, eq_bot_of_le_smul_of_le_jacobson_bot, eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator, eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot, eq_smul_of_le_smul_of_le_jacobson, exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot, exists_sub_one_mem_and_smul_le_of_fg_of_le_sup, le_of_le_smul_of_le_jacobson_bot, le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot, le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot, smul_le_of_le_smul_of_le_jacobson_bot, sup_eq_sup_smul_of_le_smul_of_le_jacobson, sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson, top_ne_ideal_smul_of_le_jacobson_annihilator, top_ne_pointwise_smul_of_mem_jacobson_annihilator, top_ne_set_smul_of_subset_jacobson_annihilator	17
Total	17

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Submodule instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ideal.jacobson CommRing.toRing annihilator	Bot.bot instBot	—	IsScalarTower.left eq_smul_of_le_smul_of_le_jacobson Eq.le annihilator_smul
eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Ideal SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson annihilator	Bot.bot instBot	—	smulCommClass_self eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator IsScalarTower.left ideal_span_singleton_smul span_singleton_le_iff_mem
eq_bot_of_le_smul_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Ideal instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot	—	—	IsScalarTower.left eq_smul_of_le_smul_of_le_jacobson bot_smul
eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Submodule pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.instHasSubset SetLike.coe Ideal Ring.toSemiring CommRing.toRing setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson annihilator	Bot.bot instBot	—	eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator IsScalarTower.left span_smul_eq span_le
eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot map HasQuotient.Quotient Submodule hasQuotient instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Quotient.addCommGroup Quotient.module RingHom.id RingHomSurjective.ids mkQ	—	—	IsScalarTower.left RingHomSurjective.ids le_antisymm le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot Eq.le comap_map_mkQ sup_of_le_right le_sup_right
eq_smul_of_le_smul_of_le_jacobson 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Ideal instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ideal.jacobson CommRing.toRing	—	—	IsScalarTower.left le_antisymm exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson neg_sub sub_smul SemigroupAction.mul_smul one_smul smul_zero sub_zero smul_mem_smul neg_mem smul_le smul_mem
exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot span HasQuotient.Quotient Submodule hasQuotient instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Quotient.addCommGroup Quotient.module map RingHom.id RingHomSurjective.ids mkQ	Set.InjOn DFunLike.coe LinearMap LinearMap.instFunLike Set.image	—	IsScalarTower.left RingHomSurjective.ids Quotient.mk_out Set.image_congr Set.image_image Set.image_id' eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot map_span
exists_sub_one_mem_and_smul_le_of_fg_of_le_sup 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice Ideal instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid Ring.toSemiring	—	IsScalarTower.left le_trans smul_le_right le_sup_right RingHomSurjective.ids le_antisymm map_sup mkQ_map_self sup_of_le_right map_mono map_smul'' Quotient.isScalarTower smulCommClass_self exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul FG.map smul_inductionOn_pointwise Quotient.mk_eq_zero Quotient.mk_smul smul_mem add_mem zero_mem
le_of_le_smul_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left sup_eq_left sup_eq_sup_smul_of_le_smul_of_le_jacobson bot_smul sup_bot_eq
le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot Submodule HasQuotient.Quotient hasQuotient instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Quotient.addCommGroup Quotient.module map RingHom.id RingHomSurjective.ids mkQ	—	—	IsScalarTower.left RingHomSurjective.ids le_of_le_smul_of_le_jacobson_bot sup_comm le_imp_le_of_le_of_le le_refl comap_map_mkQ sup_of_le_right comap_mono
le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot Submodule HasQuotient.Quotient hasQuotient instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Quotient.addCommGroup Quotient.module map RingHom.id RingHomSurjective.ids mkQ	—	—	le_of_map_mkQ_le_map_mkQ_of_le_jacobson_bot
smul_le_of_le_smul_of_le_jacobson_bot 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring instBot Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left LE.le.trans smul_le_right le_of_le_smul_of_le_jacobson_bot
sup_eq_sup_smul_of_le_smul_of_le_jacobson 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left le_antisymm sup_le le_sup_left sup_le_sup_left smul_le smul_mem comap_injective_of_surjective RingHomSurjective.ids LinearMap.range_eq_top range_mkQ comap_map_mkQ eq_smul_of_le_smul_of_le_jacobson FG.map map_smul'' le_refl sup_comm ker_mkQ comap_map_eq
sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson 📖	—	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ideal Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—	IsScalarTower.left LE.le.antisymm sup_le_sup_left smul_le_right sup_le le_sup_left sup_eq_sup_smul_of_le_smul_of_le_jacobson
top_ne_ideal_smul_of_le_jacobson_annihilator 📖	—	Ideal Ring.toSemiring CommRing.toRing Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson Module.annihilator CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	—	IsScalarTower.left top_ne_bot instNontrivial eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator Module.Finite.fg_top annihilator_top
top_ne_pointwise_smul_of_mem_jacobson_annihilator 📖	—	Ideal Ring.toSemiring CommRing.toRing SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson Module.annihilator CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	—	ne_of_ne_of_eq smulCommClass_self top_ne_set_smul_of_subset_jacobson_annihilator Set.singleton_subset_iff singleton_set_smul
top_ne_set_smul_of_subset_jacobson_annihilator 📖	—	Set Set.instHasSubset SetLike.coe Ideal Ring.toSemiring CommRing.toRing setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson Module.annihilator CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	—	ne_of_ne_of_eq IsScalarTower.left top_ne_ideal_smul_of_le_jacobson_annihilator span_le span_smul_eq

---

← Back to Index