Documentation Verification Report

RegularSequence

📁 Source: Mathlib/RingTheory/Regular/RegularSequence.lean

Statistics

Metric	Count
Definitions `ofList`, `IsRegular`, `ndrecIterModByRegular`, `ndrecIterModByRegularWithRing`, `recIterModByRegular`, `recIterModByRegularWithRing`, `IsWeaklyRegular`, `ndrecIterModByRegular`, `ndrecWithRing`, `recIterModByRegular`, `recIterModByRegularWithRing`, `quotOfListConsSMulTopEquivQuotSMulTopInner`, `quotOfListConsSMulTopEquivQuotSMulTopOuter`	13
Theorems `isRegular_congr`, `isWeaklyRegular_congr`, `map_ofList`, `ofList_append`, `ofList_cons`, `ofList_cons_smul`, `ofList_nil`, `ofList_singleton`, `isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal`, `isRegular_of_perm`, `isWeaklyRegular_of_perm_of_subset_maximalIdeal`, `isRegular_congr`, `isRegular_congr'`, `isWeaklyRegular_congr`, `isWeaklyRegular_congr'`, `cons`, `cons'`, `nil`, `nontrivial`, `of_perm_of_subset_jacobson_annihilator`, `quot_ofList_smul_nontrivial`, `toIsWeaklyRegular`, `top_ne_smul`, `cons`, `cons'`, `isWeaklyRegular_lTensor`, `isWeaklyRegular_rTensor`, `nil`, `of_perm_of_subset_jacobson_annihilator`, `prototype_perm`, `regular_mod_prev`, `eq_nil_of_isRegular_on_artinian`, `isRegular_cons_iff`, `isRegular_cons_iff'`, `isRegular_iff`, `isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator`, `isWeaklyRegular_append_iff`, `isWeaklyRegular_append_iff'`, `isWeaklyRegular_cons_iff`, `isWeaklyRegular_cons_iff'`, `isWeaklyRegular_iff`, `isWeaklyRegular_iff_Fin`, `isWeaklyRegular_map_algebraMap_iff`, `isWeaklyRegular_singleton_iff`, `map_first_exact_on_four_term_right_exact_of_isSMulRegular_last`, `quotOfListConsSMulTopEquivQuotSMulTopInner_naturality`, `smul_top_le_comap_smul_top`, `top_eq_ofList_cons_smul_iff`	48
Total	61

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_congr` 📖	mathematical	—	`RingTheory.Sequence.IsRegular`	—	`IsScalarTower.left` `RingTheory.Sequence.isRegular_iff` `Submodule.Quotient.nontrivial_iff` `AddSubgroup.normal_of_comm` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `surjective` `isWeaklyRegular_congr` `Equiv.nontrivial_congr`
`isWeaklyRegular_congr` 📖	mathematical	—	`RingTheory.Sequence.IsWeaklyRegular`	—	`IsScalarTower.left` `RingTheory.Sequence.isWeaklyRegular_iff_Fin` `AddSubgroup.normal_of_comm` `AddEquivClass.instAddMonoidHomClass` `instAddEquivClass` `surjective` `List.forall₂_take` `Equiv.forall_congr` `List.Forall₂.length_eq` `Equiv.isSMulRegular_congr` `Function.Surjective.forall` `Submodule.mkQ_surjective` `List.Forall₂.get`

Ideal

Definitions

Name	Category	Theorems
`ofList` 📖	CompOp	17 math math: `map_ofList`, `Submodule.top_eq_ofList_cons_smul_iff`, `Module.supportDim_add_length_eq_supportDim_of_isRegular`, `RingTheory.Sequence.isWeaklyRegular_iff_Fin`, `RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev`, `Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality`, `RingTheory.Sequence.isWeaklyRegular_append_iff'`, `ringKrullDim_add_length_eq_ringKrullDim_of_isRegular`, `RingTheory.Sequence.isWeaklyRegular_append_iff`, `ofList_append`, `ofList_nil`, `RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial`, `ofList_cons_smul`, `ofList_singleton`, `ofList_cons`, `RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last`, `RingTheory.Sequence.isWeaklyRegular_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_ofList` 📖	mathematical	—	`map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `ofList` `DFunLike.coe`	—	`map_span` `RingHom.instRingHomClass` `Set.ext`
`ofList_append` 📖	mathematical	—	`ofList` `Ideal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Set.ext` `span_union`
`ofList_cons` 📖	mathematical	—	`ofList` `Ideal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `Set` `Set.instSingletonSet`	—	`ofList_append` `ofList_singleton`
`ofList_cons_smul` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Submodule` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `ofList` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Submodule.pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Submodule.pointwiseDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `CommMonoid.toMonoid`	—	`IsScalarTower.left` `smulCommClass_self` `ofList_cons` `Submodule.sup_smul` `Submodule.ideal_span_singleton_smul`
`ofList_nil` 📖	mathematical	—	`ofList` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Set.eq_empty_of_forall_notMem` `span_empty`
`ofList_singleton` 📖	mathematical	—	`ofList` `span` `Set` `Set.instSingletonSet`	—	`Set.ext`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `maximalIdeal`	`RingTheory.Sequence.IsRegular` `RingTheory.Sequence.IsWeaklyRegular`	—	`bot_ne_top` `Submodule.instNontrivial` `Submodule.annihilator_eq_top_iff` `Submodule.annihilator_top` `RingTheory.Sequence.isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator` `jacobson_eq_maximalIdeal`
`isRegular_of_perm` 📖	—	`RingTheory.Sequence.IsRegular`	—	—	`IsScalarTower.left` `isWeaklyRegular_of_perm_of_subset_maximalIdeal` `le_maximalIdeal` `Submodule.top_smul` `Ideal.subset_span` `ne_of_ne_of_eq` `Set.ext`
`isWeaklyRegular_of_perm_of_subset_maximalIdeal` 📖	—	`RingTheory.Sequence.IsWeaklyRegular` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `maximalIdeal`	—	—	`RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator` `maximalIdeal_le_jacobson`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRegular_congr` 📖	mathematical	—	`RingTheory.Sequence.IsRegular`	—	`RingHomInvPair.ids` `isRegular_congr'`
`isRegular_congr'` 📖	mathematical	—	`RingTheory.Sequence.IsRegular` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`AddEquiv.isRegular_congr` `List.forall₂_map_right_iff` `List.forall₂_same` `LinearMap.map_smul'`
`isWeaklyRegular_congr` 📖	mathematical	—	`RingTheory.Sequence.IsWeaklyRegular`	—	`RingHomInvPair.ids` `isWeaklyRegular_congr'`
`isWeaklyRegular_congr'` 📖	mathematical	—	`RingTheory.Sequence.IsWeaklyRegular` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`AddEquiv.isWeaklyRegular_congr` `List.forall₂_map_right_iff` `List.forall₂_same` `LinearMap.map_smul'`

RingTheory.Sequence

Definitions

Name	Category	Theorems
`IsRegular` 📖	CompData	11 math math: `isRegular_cons_iff`, `AddEquiv.isRegular_congr`, `LinearEquiv.isRegular_congr`, `isRegular_iff`, `IsWeaklyRegular.isRegular_of_isLocalizedModule_of_mem`, `IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal`, `isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator`, `LinearEquiv.isRegular_congr'`, `IsWeaklyRegular.isRegular_of_isLocalization_of_mem`, `isRegular_cons_iff'`, `IsRegular.nil`
`IsWeaklyRegular` 📖	CompData	16 math math: `isWeaklyRegular_map_algebraMap_iff`, `isWeaklyRegular_cons_iff'`, `isWeaklyRegular_cons_iff`, `isWeaklyRegular_iff_Fin`, `isWeaklyRegular_singleton_iff`, `isWeaklyRegular_append_iff'`, `IsWeaklyRegular.nil`, `isWeaklyRegular_append_iff`, `LinearEquiv.isWeaklyRegular_congr'`, `isRegular_iff`, `IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal`, `AddEquiv.isWeaklyRegular_congr`, `LinearEquiv.isWeaklyRegular_congr`, `isWeaklyRegular_iff`, `isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator`, `IsRegular.toIsWeaklyRegular`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_nil_of_isRegular_on_artinian` 📖	—	`IsRegular`	—	—	`smulCommClass_self` `RingHomSurjective.ids` `Submodule.map_top` `LinearMap.range_eq_top` `IsArtinian.surjective_of_injective_endomorphism` `IsScalarTower.left` `isWeaklyRegular_cons_iff` `Submodule.ideal_span_singleton_smul` `Submodule.sup_smul` `Ideal.ofList_cons` `lt_top_iff_ne_top` `isRegular_iff` `ne_of_lt` `lt_of_le_of_lt` `le_sup_left`
`isRegular_cons_iff` 📖	mathematical	—	`IsRegular` `IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `QuotSMulTop` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module`	—	`IsScalarTower.left` `isRegular_iff` `isWeaklyRegular_cons_iff` `Submodule.Quotient.isScalarTower` `Submodule.top_eq_ofList_cons_smul_iff`
`isRegular_cons_iff'` 📖	mathematical	—	`IsRegular` `IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `QuotSMulTop` `Ideal.Quotient.commRing` `Submodule.Quotient.addCommGroup` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1` `IsScalarTower.left` `isRegular_iff` `isWeaklyRegular_cons_iff'` `Module.IsTorsionBySet.isScalarTower` `Module.isTorsionBy_quotient_element_smul` `Submodule.Quotient.isScalarTower` `Ideal.map_ofList` `Ideal.Quotient.algebraMap_eq` `Ideal.smul_restrictScalars` `Submodule.restrictScalars_top` `Submodule.top_eq_ofList_cons_smul_iff`
`isRegular_iff` 📖	mathematical	—	`IsRegular` `IsWeaklyRegular`	—	`IsScalarTower.left`
`isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator` 📖	mathematical	`Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `Module.annihilator` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`IsRegular` `IsWeaklyRegular`	—	`IsScalarTower.left` `isRegular_iff` `Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator` `Ideal.span_le`
`isWeaklyRegular_append_iff` 📖	mathematical	—	`IsWeaklyRegular` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`IsScalarTower.left` `IsWeaklyRegular.nil` `LinearEquiv.isWeaklyRegular_congr` `Ideal.ofList_nil` `Submodule.bot_smul` `RingHomInvPair.ids` `Submodule.Quotient.isScalarTower` `isWeaklyRegular_cons_iff`
`isWeaklyRegular_append_iff'` 📖	mathematical	—	`IsWeaklyRegular` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.ofList` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Top.top` `Submodule.instTop` `Ideal.Quotient.commRing` `Submodule.Quotient.addCommGroup` `Module.instQuotientIdealSubmoduleHSMulTop` `Ideal.instIsTwoSided_1` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike`	—	`IsScalarTower.left` `Ideal.instIsTwoSided_1` `isWeaklyRegular_append_iff` `isWeaklyRegular_map_algebraMap_iff` `Module.IsTorsionBySet.isScalarTower` `Module.isTorsionBySet_quotient_ideal_smul` `Submodule.Quotient.isScalarTower`
`isWeaklyRegular_cons_iff` 📖	mathematical	—	`IsWeaklyRegular` `IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `QuotSMulTop` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module`	—	`IsScalarTower.left` `Ideal.ofList_nil` `Submodule.bot_smul` `RingHomInvPair.ids` `Submodule.Quotient.isScalarTower` `isWeaklyRegular_iff_Fin` `Fin.forall_iff_succ` `LinearEquiv.isSMulRegular_congr`
`isWeaklyRegular_cons_iff'` 📖	mathematical	—	`IsWeaklyRegular` `IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `QuotSMulTop` `Ideal.Quotient.commRing` `Submodule.Quotient.addCommGroup` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1` `isWeaklyRegular_cons_iff` `isWeaklyRegular_map_algebraMap_iff` `Module.IsTorsionBySet.isScalarTower` `Module.isTorsionBy_quotient_element_smul` `Submodule.Quotient.isScalarTower` `IsScalarTower.left`
`isWeaklyRegular_iff` 📖	mathematical	—	`IsWeaklyRegular` `IsSMulRegular` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.instSMul`	—	`IsScalarTower.left`
`isWeaklyRegular_iff_Fin` 📖	mathematical	—	`IsWeaklyRegular` `IsSMulRegular` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.instSMul`	—	`IsScalarTower.left` `isWeaklyRegular_iff`
`isWeaklyRegular_map_algebraMap_iff` 📖	mathematical	—	`IsWeaklyRegular` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	—	`AddEquiv.isWeaklyRegular_congr` `List.forall₂_map_left_iff` `List.forall₂_same` `algebraMap_smul`
`isWeaklyRegular_singleton_iff` 📖	mathematical	—	`IsWeaklyRegular` `IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`isWeaklyRegular_cons_iff` `IsWeaklyRegular.nil`
`map_first_exact_on_four_term_right_exact_of_isSMulRegular_last` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `IsWeaklyRegular`	`HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `CommRing.toRing` `Submodule.hasQuotient` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.mapQ` `Submodule.smul_top_le_comap_smul_top` `Submodule.Quotient.instZeroQuotient`	—	`IsScalarTower.left` `Submodule.smul_top_le_comap_smul_top` `Function.Exact.iff_of_ladder_linearEquiv` `Ideal.ofList_nil` `Submodule.bot_smul` `Submodule.quot_hom_ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Submodule.Quotient.isScalarTower` `smulCommClass_self` `Submodule.Quotient.smulCommClass` `Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality` `QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last` `QuotSMulTop.map_exact` `QuotSMulTop.map_surjective`

RingTheory.Sequence.IsRegular

Definitions

Name	Category	Theorems
`ndrecIterModByRegular` 📖	CompOp	—
`ndrecIterModByRegularWithRing` 📖	CompOp	—
`recIterModByRegular` 📖	CompOp	—
`recIterModByRegularWithRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `RingTheory.Sequence.IsRegular` `QuotSMulTop` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module`	—	—	`RingTheory.Sequence.isRegular_cons_iff`
`cons'` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `RingTheory.Sequence.IsRegular` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `QuotSMulTop` `Ideal.Quotient.commRing` `Submodule.Quotient.addCommGroup` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	—	`Ideal.instIsTwoSided_1` `RingTheory.Sequence.isRegular_cons_iff'`
`nil` 📖	mathematical	—	`RingTheory.Sequence.IsRegular`	—	`RingTheory.Sequence.IsWeaklyRegular.nil` `IsScalarTower.left` `not_subsingleton` `Submodule.subsingleton_iff` `subsingleton_iff_bot_eq_top` `Submodule.bot_smul` `Ideal.ofList_nil`
`nontrivial` 📖	mathematical	`RingTheory.Sequence.IsRegular`	`Nontrivial`	—	`Function.Surjective.nontrivial` `IsScalarTower.left` `quot_ofList_smul_nontrivial` `Submodule.mkQ_surjective`
`of_perm_of_subset_jacobson_annihilator` 📖	—	`RingTheory.Sequence.IsRegular` `Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `Module.annihilator` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—	`RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator` `toIsWeaklyRegular` `Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator` `nontrivial` `Module.IsNoetherian.finite` `Ideal.span_le`
`quot_ofList_smul_nontrivial` 📖	mathematical	`RingTheory.Sequence.IsRegular`	`Nontrivial` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList`	—	`IsScalarTower.left` `Submodule.Quotient.nontrivial_iff` `ne_top_of_le_ne_top` `top_ne_smul` `smul_mono_right` `Submodule.instCovariantClassHSMulLe_1` `le_top`
`toIsWeaklyRegular` 📖	mathematical	`RingTheory.Sequence.IsRegular`	`RingTheory.Sequence.IsWeaklyRegular`	—	—
`top_ne_smul` 📖	—	`RingTheory.Sequence.IsRegular`	—	—	—

RingTheory.Sequence.IsWeaklyRegular

Definitions

Name	Category	Theorems
`ndrecIterModByRegular` 📖	CompOp	—
`ndrecWithRing` 📖	CompOp	—
`recIterModByRegular` 📖	CompOp	—
`recIterModByRegularWithRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `RingTheory.Sequence.IsWeaklyRegular` `QuotSMulTop` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Submodule.Quotient.module`	—	—	`RingTheory.Sequence.isWeaklyRegular_cons_iff`
`cons'` 📖	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `RingTheory.Sequence.IsWeaklyRegular` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `QuotSMulTop` `Ideal.Quotient.commRing` `Submodule.Quotient.addCommGroup` `Submodule` `AddCommMonoid.toAddMonoid` `Submodule.pointwiseAddCommMonoid` `Submodule.pointwiseDistribMulAction` `Top.top` `Submodule.instTop` `Module.instQuotientIdealSpanSingletonSetSubmoduleHSMulTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	—	—	`Ideal.instIsTwoSided_1` `RingTheory.Sequence.isWeaklyRegular_cons_iff'`
`isWeaklyRegular_lTensor` 📖	mathematical	`RingTheory.Sequence.IsWeaklyRegular`	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule`	—	`nil` `RingHomInvPair.ids` `cons` `IsSMulRegular.lTensor` `LinearEquiv.isWeaklyRegular_congr`
`isWeaklyRegular_rTensor` 📖	mathematical	`RingTheory.Sequence.IsWeaklyRegular`	`TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `TensorProduct.addCommGroup` `TensorProduct.instModule`	—	`nil` `RingHomInvPair.ids` `cons` `IsSMulRegular.rTensor` `LinearEquiv.isWeaklyRegular_congr`
`nil` 📖	mathematical	—	`RingTheory.Sequence.IsWeaklyRegular`	—	`IsScalarTower.left`
`of_perm_of_subset_jacobson_annihilator` 📖	—	`RingTheory.Sequence.IsWeaklyRegular` `Ideal` `Ring.toSemiring` `CommRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `Module.annihilator` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	—	`prototype_perm` `IsScalarTower.left` `Submodule.Quotient.smulCommClass` `smulCommClass_self` `Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator` `IsNoetherian.noetherian` `isNoetherian_quotient` `Ideal.jacobson_mono` `le_trans` `LinearMap.annihilator_le_of_surjective` `Submodule.mkQ_surjective` `LinearMap.annihilator_le_of_injective` `Submodule.injective_subtype`
`prototype_perm` 📖	—	`RingTheory.Sequence.IsWeaklyRegular` `Submodule.torsionBy` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Bot.bot` `Submodule.instBot`	—	—	`IsScalarTower.left` `Submodule.Quotient.smulCommClass` `smulCommClass_self` `LinearEquiv.isWeaklyRegular_congr` `Ideal.ofList_nil` `Submodule.bot_smul`
`regular_mod_prev` 📖	mathematical	`RingTheory.Sequence.IsWeaklyRegular`	`IsSMulRegular` `HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `Submodule.instTop` `Submodule.Quotient.instSMul`	—	—

Submodule

Definitions

Name	Category	Theorems
`quotOfListConsSMulTopEquivQuotSMulTopInner` 📖	CompOp	1 math math: `quotOfListConsSMulTopEquivQuotSMulTopInner_naturality`
`quotOfListConsSMulTopEquivQuotSMulTopOuter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotOfListConsSMulTopEquivQuotSMulTopInner_naturality` 📖	mathematical	—	`LinearMap.comp` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `CommRing.toRing` `AddCommGroup.toAddCommMonoid` `hasQuotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `Top.top` `instTop` `QuotSMulTop` `Quotient.addCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `Quotient.module` `Quotient.isScalarTower` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `quotOfListConsSMulTopEquivQuotSMulTopInner` `mapQ` `smul_top_le_comap_smul_top` `DFunLike.coe` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Quotient.smulCommClass` `LinearMap.instFunLike` `QuotSMulTop.map`	—	`quot_hom_ext` `IsScalarTower.left` `Quotient.isScalarTower` `RingHomCompTriple.ids` `RingHomInvPair.ids` `smul_top_le_comap_smul_top` `smulCommClass_self` `Quotient.smulCommClass`
`smul_top_le_comap_smul_top` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Top.top` `instTop` `comap` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`RingHomSurjective.ids` `IsScalarTower.left` `map_le_iff_le_comap` `map_smul''` `smul_mono_right` `instCovariantClassHSMulLe_1` `le_top`
`top_eq_ofList_cons_smul_iff` 📖	mathematical	—	`Top.top` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instTop` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ideal.ofList` `QuotSMulTop` `Quotient.addCommGroup` `CommRing.toRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `pointwiseAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `pointwiseDistribMulAction` `Quotient.module` `Quotient.isScalarTower` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Ring.toSemiring` `MulAction.toSemigroupAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`IsScalarTower.left` `Quotient.isScalarTower` `Quotient.subsingleton_iff` `Equiv.subsingleton_congr` `RingHomInvPair.ids`

---

← Back to Index