Commit 2024-06-07 06:15 614409e9

View on Github →

Chore(RingTheory/Regular): Simplify some namespaces in IsSMulRegular (#13582) Simplify some namespaces in RingTheory/Regular/IsSMulRegular

Estimated changes

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean

deleted theorem IsSMulRegular.biUnion_associatedPrimes_eq_compl_regular

deleted theorem IsSMulRegular.isSMulRegular_algebraMap_iff

deleted theorem IsSMulRegular.isSMulRegular_iff_ker_lsmul_eq_bot

deleted theorem IsSMulRegular.isSMulRegular_iff_mem_nonZeroSMulDivisors

deleted theorem IsSMulRegular.isSMulRegular_iff_smul_eq_zero_imp_eq_zero

deleted theorem IsSMulRegular.isSMulRegular_of_isSMulRegular_on_submodule_on_quotient

deleted theorem IsSMulRegular.isSMulRegular_of_ker_lsmul_eq_bot

deleted theorem IsSMulRegular.isSMulRegular_of_range_eq_ker

deleted theorem IsSMulRegular.isSMulRegular_of_smul_eq_zero_imp_eq_zero

deleted theorem IsSMulRegular.isSMulRegular_on_quot_iff_lsmul_comap_eq

deleted theorem IsSMulRegular.isSMulRegular_on_quot_iff_lsmul_comap_le

deleted theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_mem_implies_mem

added theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul

deleted theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul_of_isSMulRegular

deleted theorem IsSMulRegular.isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule

deleted theorem IsSMulRegular.isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero

modified theorem IsSMulRegular.lTensor

deleted theorem IsSMulRegular.mem_of_isSMulRegular_on_quot_of_smul_mem

modified theorem IsSMulRegular.rTensor

deleted theorem IsSMulRegular.smul_top_inf_eq_smul_of_isSMulRegular_on_quot

modified theorem IsSMulRegular.submodule

modified theorem QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last

added theorem biUnion_associatedPrimes_eq_compl_regular

added theorem isSMulRegular_algebraMap_iff

added theorem isSMulRegular_iff_ker_lsmul_eq_bot

added theorem isSMulRegular_iff_mem_nonZeroSMulDivisors

added theorem isSMulRegular_iff_smul_eq_zero_imp_eq_zero

added theorem isSMulRegular_of_isSMulRegular_on_submodule_on_quotient

added theorem isSMulRegular_of_ker_lsmul_eq_bot

added theorem isSMulRegular_of_range_eq_ker

added theorem isSMulRegular_of_smul_eq_zero_imp_eq_zero

added theorem isSMulRegular_on_quot_iff_lsmul_comap_eq

added theorem isSMulRegular_on_quot_iff_lsmul_comap_le

added theorem isSMulRegular_on_quot_iff_smul_mem_implies_mem

added theorem isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule

added theorem isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero

added theorem mem_of_isSMulRegular_on_quot_of_smul_mem

added theorem smul_top_inf_eq_smul_of_isSMulRegular_on_quot

Modified Mathlib/RingTheory/Regular/RegularSequence.lean