Commit 2023-05-23 13:58 f1455f1d

View on Github →

feat: port RingTheory.Ideal.Over (#4270)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.IntegralClosure.comap_lt_comap

added theorem Ideal.IntegralClosure.comap_ne_bot

added theorem Ideal.IntegralClosure.eq_bot_of_comap_eq_bot

added theorem Ideal.IntegralClosure.isMaximal_of_isMaximal_comap

added theorem Ideal.IsIntegralClosure.comap_lt_comap

added theorem Ideal.IsIntegralClosure.comap_ne_bot

added theorem Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot

added theorem Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap

added theorem Ideal.Quotient.algebraMap_quotient_map_quotient

added def Ideal.Quotient.algebraQuotientOfLeComap

added theorem Ideal.Quotient.mk_smul_mk_quotient_map_quotient

added theorem Ideal.coeff_zero_mem_comap_of_root_mem

added theorem Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem

added theorem Ideal.comap_eq_of_scalar_tower_quotient

added theorem Ideal.comap_lt_comap_of_integral_mem_sdiff

added theorem Ideal.comap_lt_comap_of_root_mem_sdiff

added theorem Ideal.comap_ne_bot_of_algebraic_mem

added theorem Ideal.comap_ne_bot_of_integral_mem

added theorem Ideal.comap_ne_bot_of_root_mem

added theorem Ideal.eq_bot_of_comap_eq_bot

added theorem Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff

added theorem Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem

added theorem Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem

added theorem Ideal.exists_ideal_over_maximal_of_isIntegral

added theorem Ideal.exists_ideal_over_prime_of_isIntegral

added theorem Ideal.exists_ideal_over_prime_of_is_integral'

added theorem Ideal.exists_nonzero_mem_of_ne_bot

added theorem Ideal.injective_quotient_le_comap_map

added theorem Ideal.isMaximal_comap_of_isIntegral_of_isMaximal

added theorem Ideal.isMaximal_comap_of_isIntegral_of_is_maximal'

added theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'

added theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap

added theorem Ideal.mem_of_one_mem

added theorem Ideal.quotient_mk_maps_eq