Nakayama

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

Statistics

Metric	Count
Definitions	0
Theorems exists_mem_and_smul_eq_self_of_fg_of_le_smul, exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul	2
Total	2

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_and_smul_eq_self_of_fg_of_le_smul 📖	mathematical	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	SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	IsScalarTower.left exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul neg_mem neg_sub sub_smul one_smul
exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul 📖	mathematical	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	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 SubNegMonoid.toAddMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsScalarTower.left fg_def smulCommClass_self sub_self Ideal.zero_mem mem_comap one_smul span_le le_refl Set.Finite.induction_on mem_bot smul_bot span_empty mem_sup smul_sup span_union Set.singleton_union Set.insert_subset_iff mem_smul_span_singleton Ideal.instIsTwoSided_1 sub_right_comm Ideal.sub_mem sub_smul add_sub_cancel_left mul_sub mul_one sub_add_sub_cancel Ideal.add_mem Ideal.mul_mem_left SemigroupAction.mul_smul smul_add smul_smul mul_comm AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass smul_mem

---

← Back to Index