Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-05 09:32 e24808b3

View on Github →

feat(ring_theory/filtration): Artin-Rees lemma and Krull's intersection theorems (#16000)

Estimated changes

Modified src/ring_theory/filtration.lean

added theorem ideal.exists_pow_inf_eq_pow_smul

added theorem ideal.filtration.inf_submodule

added theorem ideal.filtration.mem_submodule

added theorem ideal.filtration.stable.inter_left

added theorem ideal.filtration.stable.inter_right

added theorem ideal.filtration.stable.of_le

added def ideal.filtration.submodule

added theorem ideal.filtration.submodule_closure_single

added theorem ideal.filtration.submodule_eq_span_le_iff_stable_ge

added theorem ideal.filtration.submodule_fg_iff_stable

added def ideal.filtration.submodule_inf_hom

added theorem ideal.filtration.submodule_span_single

added theorem ideal.infi_pow_eq_bot_of_is_domain

added theorem ideal.infi_pow_eq_bot_of_local_ring

added theorem ideal.infi_pow_smul_eq_bot_of_local_ring

added theorem ideal.mem_infi_smul_pow_eq_bot_iff

Modified src/ring_theory/noetherian.lean

added theorem submodule.fg.stablizes_of_supr_eq