Commit 2024-06-06 07:41 322601e1

View on Github →

Feat: Add regular sequences (#12544) Add the definition of regular sequences and induction principles for them.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Regular/RegularSequence.lean

added theorem AddEquiv.isRegular_congr

added theorem AddEquiv.isWeaklyRegular_congr

added theorem Ideal.map_ofList

added theorem Ideal.ofList_append

added theorem Ideal.ofList_cons

added theorem Ideal.ofList_cons_smul

added theorem Ideal.ofList_nil

added theorem Ideal.ofList_singleton

added theorem LinearEquiv.isRegular_congr'

added theorem LinearEquiv.isRegular_congr

added theorem LinearEquiv.isWeaklyRegular_congr'

added theorem LinearEquiv.isWeaklyRegular_congr

added theorem LocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal

added theorem LocalRing.isRegular_of_perm

added theorem LocalRing.isWeaklyRegular_of_perm_of_subset_maximalIdeal

added theorem RingTheory.Sequence.IsRegular.cons'

added theorem RingTheory.Sequence.IsRegular.cons

added def RingTheory.Sequence.IsRegular.ndrecIterModByRegular

added def RingTheory.Sequence.IsRegular.ndrecIterModByRegularWithRing

added theorem RingTheory.Sequence.IsRegular.nil

added theorem RingTheory.Sequence.IsRegular.nontrivial

added theorem RingTheory.Sequence.IsRegular.of_perm_of_subset_jacobson_annihilator

added theorem RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial

added def RingTheory.Sequence.IsRegular.recIterModByRegular

added def RingTheory.Sequence.IsRegular.recIterModByRegularWithRing

added structure RingTheory.Sequence.IsRegular

added theorem RingTheory.Sequence.IsWeaklyRegular.cons'

added theorem RingTheory.Sequence.IsWeaklyRegular.cons

added theorem RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_lTensor

added theorem RingTheory.Sequence.IsWeaklyRegular.isWeaklyRegular_rTensor

added def RingTheory.Sequence.IsWeaklyRegular.ndrecIterModByRegular

added def RingTheory.Sequence.IsWeaklyRegular.ndrecWithRing

added theorem RingTheory.Sequence.IsWeaklyRegular.nil

added theorem RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator

added theorem RingTheory.Sequence.IsWeaklyRegular.prototype_perm

added def RingTheory.Sequence.IsWeaklyRegular.recIterModByRegular

added def RingTheory.Sequence.IsWeaklyRegular.recIterModByRegularWithRing

added structure RingTheory.Sequence.IsWeaklyRegular

added theorem RingTheory.Sequence.eq_nil_of_isRegular_on_artinian

added theorem RingTheory.Sequence.isRegular_cons_iff'

added theorem RingTheory.Sequence.isRegular_cons_iff

added theorem RingTheory.Sequence.isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator

added theorem RingTheory.Sequence.isWeaklyRegular_append_iff'

added theorem RingTheory.Sequence.isWeaklyRegular_append_iff

added theorem RingTheory.Sequence.isWeaklyRegular_cons_iff'

added theorem RingTheory.Sequence.isWeaklyRegular_cons_iff

added theorem RingTheory.Sequence.isWeaklyRegular_iff_Fin

added theorem RingTheory.Sequence.isWeaklyRegular_map_algebraMap_iff

added theorem RingTheory.Sequence.isWeaklyRegular_singleton_iff

added theorem RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last

added def Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner

added theorem Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality

added def Submodule.quotOfListConsSMulTopEquivQuotSMulTopOuter

added theorem Submodule.smul_top_le_comap_smul_top

added theorem Submodule.top_eq_ofList_cons_smul_iff