Commit 2023-06-01 12:52 c639b48c

View on Github →

feat: port RingTheory.Filtration (#4488)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Filtration.lean

added theorem Ideal.Filtration.Stable.bounded_difference

added theorem Ideal.Filtration.Stable.exists_forall_le

added theorem Ideal.Filtration.Stable.exists_pow_smul_eq

added theorem Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge

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.Stable

added theorem Ideal.Filtration.bot_N

added theorem Ideal.Filtration.iInf_N

added theorem Ideal.Filtration.iSup_N

added theorem Ideal.Filtration.inf_N

added theorem Ideal.Filtration.inf_submodule

added theorem Ideal.Filtration.mem_submodule

added theorem Ideal.Filtration.pow_smul_le

added theorem Ideal.Filtration.pow_smul_le_pow_smul

added theorem Ideal.Filtration.sInf_N

added theorem Ideal.Filtration.sSup_N

added theorem Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge

added def Ideal.Filtration.submoduleInfHom

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 theorem Ideal.Filtration.submodule_span_single

added theorem Ideal.Filtration.sup_N

added theorem Ideal.Filtration.top_N

added structure Ideal.Filtration

added theorem Ideal.exists_pow_inf_eq_pow_smul

added theorem Ideal.iInf_pow_eq_bot_of_isDomain

added theorem Ideal.iInf_pow_eq_bot_of_localRing

added theorem Ideal.iInf_pow_smul_eq_bot_of_localRing

added theorem Ideal.mem_iInf_smul_pow_eq_bot_iff

added def Ideal.stableFiltration

added theorem Ideal.stableFiltration_stable

added def Ideal.trivialFiltration