Commit 2024-06-05 04:24 ddfa53da

View on Github →

Ring-specific lemmas about regular elements (#13360) Add lemmas about regular elements from commutative algebra.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Regular/SMul.lean

deleted theorem IsSMulRegular.isSMulRegular_of_injective_of_isSMulRegular

added theorem IsSMulRegular.of_injective

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added theorem LinearMap.lsmul_eq_DistribMulAction_toLinearMap

Modified Mathlib/RingTheory/Nakayama.lean

added theorem Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator

added theorem Submodule.eq_bot_of_eq_pointwise_smul_of_mem_jacobson_annihilator

added theorem Submodule.eq_bot_of_set_smul_eq_of_subset_jacobson_annihilator

added theorem Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator

added theorem Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator

added theorem Submodule.top_ne_set_smul_of_subset_jacobson_annihilator

Created Mathlib/RingTheory/QuotSMulTop.lean

added theorem QuotSMulTop.equivQuotTensor_naturality

added theorem QuotSMulTop.equivQuotTensor_naturality_mk

added theorem QuotSMulTop.equivTensorQuot_naturality

added theorem QuotSMulTop.equivTensorQuot_naturality_mk

added def QuotSMulTop.map

added theorem QuotSMulTop.map_apply_mk

added theorem QuotSMulTop.map_comp

added theorem QuotSMulTop.map_comp_mkQ

added theorem QuotSMulTop.map_exact

added theorem QuotSMulTop.map_id

added theorem QuotSMulTop.map_surjective

Created Mathlib/RingTheory/Regular/IsSMulRegular.lean

added theorem IsSMulRegular.biUnion_associatedPrimes_eq_compl_regular

added theorem IsSMulRegular.isSMulRegular_algebraMap_iff

added theorem IsSMulRegular.isSMulRegular_iff_ker_lsmul_eq_bot

added theorem IsSMulRegular.isSMulRegular_iff_mem_nonZeroSMulDivisors

added theorem IsSMulRegular.isSMulRegular_iff_smul_eq_zero_imp_eq_zero

added theorem IsSMulRegular.isSMulRegular_of_isSMulRegular_on_submodule_on_quotient

added theorem IsSMulRegular.isSMulRegular_of_ker_lsmul_eq_bot

added theorem IsSMulRegular.isSMulRegular_of_range_eq_ker

added theorem IsSMulRegular.isSMulRegular_of_smul_eq_zero_imp_eq_zero

added theorem IsSMulRegular.isSMulRegular_on_quot_iff_lsmul_comap_eq

added theorem IsSMulRegular.isSMulRegular_on_quot_iff_lsmul_comap_le

added theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_mem_implies_mem

added theorem IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul_of_isSMulRegular

added theorem IsSMulRegular.isSMulRegular_on_submodule_iff_disjoint_ker_lsmul_submodule

added theorem IsSMulRegular.isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero

added theorem IsSMulRegular.lTensor

added theorem IsSMulRegular.mem_of_isSMulRegular_on_quot_of_smul_mem

added theorem IsSMulRegular.rTensor

added theorem IsSMulRegular.smul_top_inf_eq_smul_of_isSMulRegular_on_quot

added theorem IsSMulRegular.submodule

added theorem LinearEquiv.isSMulRegular_congr'

added theorem LinearEquiv.isSMulRegular_congr

added theorem QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last