Commit 2023-06-05 16:53 f08cd344

View on Github →

feat: port RingTheory.DedekindDomain.Ideal (#4630)

An instance from RingTheory.FractionalIdeal was used explicitly so I had to give it a name
At three places, an equiv is defined and the lemmas produced by [simps] (or [simps!]) make the simpNF linter very unhappy so I commented out the [simps] and left a porting note

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem Associates.le_singleton_iff

added theorem FractionalIdeal.adjoinIntegral_eq_one_of_isUnit

added theorem FractionalIdeal.coe_ideal_le_self_mul_inv

added theorem FractionalIdeal.coe_ideal_mul_inv

added theorem FractionalIdeal.coe_ideal_span_singleton_div_self

added theorem FractionalIdeal.coe_ideal_span_singleton_inv_mul

added theorem FractionalIdeal.coe_ideal_span_singleton_mul_inv

added theorem FractionalIdeal.coe_inv_of_nonzero

added theorem FractionalIdeal.exists_not_mem_one_of_ne_bot

added theorem FractionalIdeal.inv_anti_mono

added theorem FractionalIdeal.inv_eq

added theorem FractionalIdeal.inv_nonzero

added theorem FractionalIdeal.inv_zero'

added theorem FractionalIdeal.invertible_iff_generator_nonzero

added theorem FractionalIdeal.invertible_of_principal

added theorem FractionalIdeal.isPrincipal_inv

added theorem FractionalIdeal.le_self_mul_inv

added theorem FractionalIdeal.map_inv

added theorem FractionalIdeal.mem_inv_iff

added theorem FractionalIdeal.mul_generator_self_inv

added theorem FractionalIdeal.mul_inv_cancel_iff

added theorem FractionalIdeal.mul_inv_cancel_iff_isUnit

added theorem FractionalIdeal.mul_inv_cancel_of_le_one

added theorem FractionalIdeal.mul_left_le_iff

added theorem FractionalIdeal.mul_left_strictMono

added theorem FractionalIdeal.mul_right_le_iff

added theorem FractionalIdeal.mul_right_strictMono

added theorem FractionalIdeal.one_mem_inv_coe_ideal

added theorem FractionalIdeal.right_inverse_eq

added theorem FractionalIdeal.spanSingleton_div_self

added theorem FractionalIdeal.spanSingleton_div_spanSingleton

added theorem FractionalIdeal.spanSingleton_inv

added theorem FractionalIdeal.spanSingleton_inv_mul

added theorem FractionalIdeal.spanSingleton_mul_inv

added theorem Ideal.IsPrime.mul_mem_pow

added theorem Ideal.coprime_of_no_prime_ge

added theorem Ideal.count_normalizedFactors_eq

added theorem Ideal.dvdNotUnit_iff_lt

added theorem Ideal.dvd_iff_le

added theorem Ideal.dvd_span_singleton

added theorem Ideal.eq_prime_pow_of_succ_lt_of_le

added theorem Ideal.exist_integer_multiples_not_mem

added theorem Ideal.exists_mem_pow_not_mem_pow_succ

added theorem Ideal.gcd_eq_sup

added theorem Ideal.inf_eq_mul_of_coprime

added theorem Ideal.isPrime_iff_bot_or_prime

added theorem Ideal.isPrime_of_prime

added theorem Ideal.lcm_eq_inf

added theorem Ideal.le_mul_of_no_prime_factors

added theorem Ideal.le_of_pow_le_prime

added theorem Ideal.pow_le_prime_iff

added theorem Ideal.pow_lt_self

added theorem Ideal.pow_succ_lt_pow

added theorem Ideal.prime_iff_isPrime

added theorem Ideal.prime_of_isPrime

added theorem Ideal.prod_le_prime

added theorem Ideal.strictAnti_pow

added theorem Ideal.sup_mul_inf

added theorem IsDedekindDomain.HeightOneSpectrum.associates_irreducible

added def IsDedekindDomain.HeightOneSpectrum.equivMaximalSpectrum

added theorem IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot

added theorem IsDedekindDomain.HeightOneSpectrum.irreducible

added theorem IsDedekindDomain.HeightOneSpectrum.prime

added structure IsDedekindDomain.HeightOneSpectrum

added theorem IsDedekindDomain.exists_forall_sub_mem_ideal

added theorem IsDedekindDomain.exists_representative_mod_finset

added theorem IsDedekindDomain.inf_prime_pow_eq_prod

added theorem IsDedekindDomain.quotientEquivPiFactors_mk

added theorem IsDedekindDomainInv.dimensionLeOne

added theorem IsDedekindDomainInv.integrallyClosed

added theorem IsDedekindDomainInv.inv_mul_eq_one

added theorem IsDedekindDomainInv.isDedekindDomain

added theorem IsDedekindDomainInv.isNoetherianRing

added theorem IsDedekindDomainInv.mul_inv_eq_one

added def IsDedekindDomainInv

added theorem Ring.DimensionLeOne.prime_le_prime_iff_eq

added theorem count_le_of_ideal_ge

added theorem exists_multiset_prod_cons_le_and_prod_not_le

added def idealFactorsEquivOfQuotEquiv

added theorem idealFactorsEquivOfQuotEquiv_is_dvd_iso

added theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors

added theorem idealFactorsEquivOfQuotEquiv_symm

added def idealFactorsFunOfQuotHom

added theorem idealFactorsFunOfQuotHom_comp

added theorem idealFactorsFunOfQuotHom_id

added theorem irreducible_pow_sup

added theorem irreducible_pow_sup_of_ge

added theorem irreducible_pow_sup_of_le

added theorem isDedekindDomainInv_iff

added theorem isDedekindDomain_iff_isDedekindDomainInv

added theorem multiplicity_eq_multiplicity_span

added theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity

added theorem multiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_multiplicity

added def normalizedFactorsEquivOfQuotEquiv

added theorem normalizedFactorsEquivOfQuotEquiv_multiplicity_eq_multiplicity

added theorem normalizedFactorsEquivOfQuotEquiv_symm

added theorem prod_normalizedFactors_eq_self

added theorem singleton_span_mem_normalizedFactors_of_mem_normalizedFactors

added theorem span_singleton_dvd_span_singleton_iff_dvd

added theorem sup_eq_prod_inf_factors

Modified Mathlib/RingTheory/FractionalIdeal.lean