Commit 2023-03-09 08:23 f863c3c9

View on Github →

feat: port RingTheory.Ideal.Operations (#2701)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Operations.lean

added theorem Associates.mk_ne_zero'

added theorem Basis.mem_ideal_iff'

added theorem Basis.mem_ideal_iff

added def Ideal.IsPrimary

added theorem Ideal.IsPrime.inf_le'

added theorem Ideal.IsPrime.inf_le

added theorem Ideal.IsPrime.isPrimary

added theorem Ideal.IsPrime.isRadical

added theorem Ideal.IsPrime.mul_le

added theorem Ideal.IsPrime.multiset_prod_le

added theorem Ideal.IsPrime.multiset_prod_map_le

added theorem Ideal.IsPrime.prod_le

added theorem Ideal.IsPrime.radical

added theorem Ideal.IsPrime.radical_le_iff

added theorem Ideal.IsRadical.comap

added theorem Ideal.IsRadical.radical_le_iff

added def Ideal.IsRadical

added theorem Ideal.RingEquiv.bot_maximal_iff

added theorem Ideal.add_eq_sup

added theorem Ideal.apply_coe_mem_map

added theorem Ideal.basisSpanSingleton_apply

added theorem Ideal.bot_mul

added theorem Ideal.coe_comap

added theorem Ideal.coe_restrictScalars

added def Ideal.comap

added theorem Ideal.comap_Inf'

added theorem Ideal.comap_bot_le_of_injective

added theorem Ideal.comap_bot_of_injective

added theorem Ideal.comap_comap

added theorem Ideal.comap_eq_top_iff

added theorem Ideal.comap_id

added theorem Ideal.comap_inf

added theorem Ideal.comap_infᵢ

added theorem Ideal.comap_infₛ

added theorem Ideal.comap_injective_of_surjective

added theorem Ideal.comap_isMaximal_of_surjective

added theorem Ideal.comap_isPrime

added theorem Ideal.comap_le_comap_iff_of_surjective

added theorem Ideal.comap_le_iff_le_map

added theorem Ideal.comap_le_map_of_inv_on

added theorem Ideal.comap_le_map_of_inverse

added theorem Ideal.comap_map_comap

added theorem Ideal.comap_map_of_surjective

added theorem Ideal.comap_mono

added theorem Ideal.comap_ne_top

added theorem Ideal.comap_of_equiv

added theorem Ideal.comap_radical

added theorem Ideal.comap_top

added theorem Ideal.constr_basisSpanSingleton

added theorem Ideal.eq_span_singleton_mul

added theorem Ideal.finset_inf_span_singleton

added theorem Ideal.finsuppTotal_apply

added theorem Ideal.finsuppTotal_apply_eq_of_fintype

added theorem Ideal.gc_map_comap

added def Ideal.giMapComap

added theorem Ideal.infᵢ_span_singleton

added theorem Ideal.infᵢ_sup_eq_top

added theorem Ideal.isPrimary_inf

added theorem Ideal.isPrime_radical

added theorem Ideal.isRadical_bot_of_noZeroDivisors

added theorem Ideal.isUnit_iff

added theorem Ideal.ker_le_comap

added theorem Ideal.le_comap_map

added theorem Ideal.le_comap_mul

added theorem Ideal.le_comap_of_map_le

added theorem Ideal.le_comap_pow

added theorem Ideal.le_comap_sup

added theorem Ideal.le_map_of_comap_le_of_surjective

added theorem Ideal.le_of_dvd

added theorem Ideal.le_radical

added theorem Ideal.le_span_singleton_mul_iff

added theorem Ideal.map.isMaximal

added def Ideal.map

added def Ideal.mapHom

added theorem Ideal.map_bot

added theorem Ideal.map_comap_le

added theorem Ideal.map_comap_map

added theorem Ideal.map_comap_of_equiv

added theorem Ideal.map_comap_of_surjective

added theorem Ideal.map_eq_bot_iff_le_ker

added theorem Ideal.map_eq_bot_iff_of_injective

added theorem Ideal.map_eq_iff_sup_ker_eq_of_surjective

added theorem Ideal.map_eq_submodule_map

added theorem Ideal.map_eq_top_or_isMaximal_of_surjective

added theorem Ideal.map_id

added theorem Ideal.map_inf_comap_of_surjective

added theorem Ideal.map_inf_le

added theorem Ideal.map_infᵢ_comap_of_surjective

added theorem Ideal.map_infₛ

added theorem Ideal.map_isPrime_of_equiv

added theorem Ideal.map_isPrime_of_surjective

added theorem Ideal.map_le_comap_of_inv_on

added theorem Ideal.map_le_comap_of_inverse

added theorem Ideal.map_le_iff_le_comap

added theorem Ideal.map_le_of_le_comap

added theorem Ideal.map_map

added theorem Ideal.map_mono

added theorem Ideal.map_mul

added theorem Ideal.map_of_equiv

added theorem Ideal.map_radical_le

added theorem Ideal.map_radical_of_surjective

added theorem Ideal.map_span

added theorem Ideal.map_sup

added theorem Ideal.map_sup_comap_of_surjective

added theorem Ideal.map_supᵢ

added theorem Ideal.map_supᵢ_comap_of_surjective

added theorem Ideal.map_supₛ

added theorem Ideal.map_surjective_of_surjective

added theorem Ideal.map_top

added theorem Ideal.mem_colon_singleton

added theorem Ideal.mem_comap

added theorem Ideal.mem_image_of_mem_map_of_surjective

added theorem Ideal.mem_map_iff_of_surjective

added theorem Ideal.mem_map_of_mem

added theorem Ideal.mem_mul_span_singleton

added theorem Ideal.mem_radical_of_pow_mem

added theorem Ideal.mem_span_singleton_mul

added theorem Ideal.mul_bot

added theorem Ideal.mul_eq_bot

added theorem Ideal.mul_eq_inf_of_coprime

added theorem Ideal.mul_le

added theorem Ideal.mul_le_inf

added theorem Ideal.mul_le_left

added theorem Ideal.mul_le_right

added theorem Ideal.mul_left_self_sup

added theorem Ideal.mul_mem_mul

added theorem Ideal.mul_mem_mul_rev

added theorem Ideal.mul_mono

added theorem Ideal.mul_mono_left

added theorem Ideal.mul_mono_right

added theorem Ideal.mul_right_self_sup

added theorem Ideal.mul_sup

added theorem Ideal.mul_sup_eq_of_coprime_left

added theorem Ideal.mul_sup_eq_of_coprime_right

added theorem Ideal.mul_top

added theorem Ideal.multiset_prod_le_inf

added theorem Ideal.multiset_prod_span_singleton

added theorem Ideal.one_eq_top

added def Ideal.orderEmbeddingOfSurjective

added theorem Ideal.pow_le_pow

added theorem Ideal.pow_le_self

added theorem Ideal.pow_mem_pow

added theorem Ideal.pow_mono

added theorem Ideal.pow_sup_eq_top

added theorem Ideal.pow_sup_pow_eq_top

added theorem Ideal.prod_eq_bot

added theorem Ideal.prod_le_inf

added theorem Ideal.prod_mem_prod

added theorem Ideal.prod_span

added theorem Ideal.prod_span_singleton

added theorem Ideal.prod_sup_eq_top

added def Ideal.radical

added theorem Ideal.radical_bot_of_noZeroDivisors

added theorem Ideal.radical_eq_iff

added theorem Ideal.radical_eq_infₛ

added theorem Ideal.radical_eq_top

added theorem Ideal.radical_idem

added theorem Ideal.radical_inf

added theorem Ideal.radical_isRadical

added theorem Ideal.radical_le_radical_iff

added theorem Ideal.radical_mono

added theorem Ideal.radical_mul

added theorem Ideal.radical_pow

added theorem Ideal.radical_sup

added theorem Ideal.radical_top

added theorem Ideal.range_finsuppTotal

added def Ideal.relIsoOfBijective

added def Ideal.relIsoOfSurjective

added theorem Ideal.restrictScalars_mul

added theorem Ideal.smul_top_eq_map

added theorem Ideal.span_mul_span'

added theorem Ideal.span_mul_span

added theorem Ideal.span_pair_mul_span_pair

added theorem Ideal.span_singleton_mul_eq_span_singleton_mul

added theorem Ideal.span_singleton_mul_le_iff

added theorem Ideal.span_singleton_mul_le_span_singleton_mul

added theorem Ideal.span_singleton_mul_left_inj

added theorem Ideal.span_singleton_mul_left_injective

added theorem Ideal.span_singleton_mul_left_mono

added theorem Ideal.span_singleton_mul_right_inj

added theorem Ideal.span_singleton_mul_right_injective

added theorem Ideal.span_singleton_mul_right_mono

added theorem Ideal.span_singleton_mul_span_singleton

added theorem Ideal.span_singleton_pow

added theorem Ideal.subset_union

added theorem Ideal.subset_union_prime'

added theorem Ideal.subset_union_prime

added theorem Ideal.sum_eq_sup

added theorem Ideal.sup_eq_top_iff_isCoprime

added theorem Ideal.sup_infᵢ_eq_top

added theorem Ideal.sup_mul

added theorem Ideal.sup_mul_eq_of_coprime_left

added theorem Ideal.sup_mul_eq_of_coprime_right

added theorem Ideal.sup_mul_left_self

added theorem Ideal.sup_mul_right_self

added theorem Ideal.sup_pow_eq_top

added theorem Ideal.sup_prod_eq_top

added theorem Ideal.top_mul

added theorem Ideal.top_pow

added theorem Ideal.zero_eq_bot

added theorem RingHom.comap_ker

added theorem RingHom.eq_liftOfRightInverse

added theorem RingHom.injective_iff_ker_eq_bot

added def RingHom.ker

added theorem RingHom.ker_coe_equiv

added theorem RingHom.ker_eq

added theorem RingHom.ker_eq_bot_iff_eq_zero

added theorem RingHom.ker_eq_comap_bot

added theorem RingHom.ker_equiv

added theorem RingHom.ker_isMaximal_of_surjective

added theorem RingHom.ker_isPrime

added theorem RingHom.ker_ne_top

added def RingHom.liftOfRightInverse

added def RingHom.liftOfRightInverseAux

added theorem RingHom.liftOfRightInverseAux_comp_apply

added theorem RingHom.liftOfRightInverse_comp

added theorem RingHom.liftOfRightInverse_comp_apply

added theorem RingHom.mem_ker

added theorem RingHom.not_one_mem_ker

added theorem RingHom.sub_mem_ker_iff

added def Submodule.annihilator

added theorem Submodule.annihilator_bot

added theorem Submodule.annihilator_eq_top_iff

added theorem Submodule.annihilator_mono

added theorem Submodule.annihilator_mul

added theorem Submodule.annihilator_smul

added theorem Submodule.annihilator_supᵢ

added theorem Submodule.bot_smul

added def Submodule.colon

added theorem Submodule.colon_mono

added theorem Submodule.ideal_span_singleton_smul

added theorem Submodule.infᵢ_colon_supᵢ

added theorem Submodule.map_le_smul_top

added theorem Submodule.map_smul''

added theorem Submodule.mem_annihilator'

added theorem Submodule.mem_annihilator

added theorem Submodule.mem_annihilator_span

added theorem Submodule.mem_annihilator_span_singleton

added theorem Submodule.mem_colon'

added theorem Submodule.mem_colon

added theorem Submodule.mem_colon_singleton

added theorem Submodule.mem_ideal_smul_span_iff_exists_sum'

added theorem Submodule.mem_ideal_smul_span_iff_exists_sum

added theorem Submodule.mem_of_span_eq_top_of_smul_pow_mem

added theorem Submodule.mem_of_span_top_of_smul_mem

added theorem Submodule.mem_smul_span

added theorem Submodule.mem_smul_span_singleton

added theorem Submodule.mem_smul_top_iff

added theorem Submodule.mul_annihilator

added theorem Submodule.smul_bot

added theorem Submodule.smul_comap_le_comap_smul

added theorem Submodule.smul_induction_on'

added theorem Submodule.smul_induction_on

added theorem Submodule.smul_inf_le

added theorem Submodule.smul_infᵢ_le

added theorem Submodule.smul_le

added theorem Submodule.smul_le_right

added theorem Submodule.smul_mem_smul

added theorem Submodule.smul_mono

added theorem Submodule.smul_mono_left

added theorem Submodule.smul_mono_right

added theorem Submodule.smul_sup

added theorem Submodule.smul_supᵢ

added theorem Submodule.span_smul_span

added theorem Submodule.sup_smul

added theorem Submodule.top_smul