Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-08 09:29 2f38ed7a

View on Github →

feat(ring_theory/ideal_operations): define ideal operations (multiplication and radical) (#462)

Estimated changes

Modified group_theory/free_abelian_group.lean

Modified linear_algebra/basic.lean

added theorem submodule.mem_Sup_of_directed

added theorem submodule.mem_map_of_mem

Modified linear_algebra/tensor_product.lean

Modified order/order_iso.lean

Modified order/zorn.lean

added theorem zorn.zorn_partial_order₀

Created ring_theory/ideal_operations.lean

added theorem ideal.add_eq_sup

added theorem ideal.bot_mul

added def ideal.comap

added theorem ideal.comap_inf

added theorem ideal.comap_mono

added theorem ideal.comap_ne_top

added theorem ideal.comap_radical

added theorem ideal.comap_top

added theorem ideal.is_prime.radical

added theorem ideal.is_prime.radical_le_iff

added theorem ideal.le_comap_mul

added theorem ideal.le_comap_sup

added theorem ideal.le_radical

added def ideal.map

added theorem ideal.map_bot

added theorem ideal.map_inf_le

added theorem ideal.map_le_iff_le_comap

added theorem ideal.map_mono

added theorem ideal.map_mul

added theorem ideal.map_radical_le

added theorem ideal.map_sup

added theorem ideal.map_top

added theorem ideal.mem_comap

added theorem ideal.mem_map_of_mem

added theorem ideal.mul_bot

added theorem ideal.mul_eq_inf_of_coprime

added theorem ideal.mul_le

added theorem ideal.mul_le_inf

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_sup

added theorem ideal.mul_top

added theorem ideal.one_eq_top

added def ideal.radical

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_mono

added theorem ideal.radical_mul

added theorem ideal.radical_pow

added theorem ideal.radical_sup

added theorem ideal.radical_top

added theorem ideal.span_mul_span

added theorem ideal.sup_mul

added theorem ideal.top_mul

added theorem ideal.zero_eq_bot

added theorem submodule.add_eq_sup

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_supr

added theorem submodule.bot_smul

added def submodule.colon

added theorem submodule.colon_mono

added theorem submodule.infi_colon_supr

added theorem submodule.mem_annihilator'

added theorem submodule.mem_annihilator

added theorem submodule.mem_colon'

added theorem submodule.mem_colon

added theorem submodule.smul_assoc

added theorem submodule.smul_bot

added theorem submodule.smul_induction_on

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

added theorem submodule.sup_smul

added theorem submodule.top_smul

added theorem submodule.zero_eq_bot

Modified ring_theory/ideals.lean

deleted def ideal.comap

deleted theorem ideal.comap_ne_top

added theorem ideal.is_prime.mem_of_pow_mem

deleted theorem ideal.mem_comap