Commit 2024-03-27 11:32 85b063b5

View on Github →

feat(DedekindDomain.Ideal): remove Domain assumption from DedekindDomain (#11527) Probably because in mathlib4 the definition IsDedekindDomain extends Domain, and this was not the case in mathlib3, there are unused hypothesis of the form

variable [IsDomain R] [IsDedekindDomain R]

and this PR removes the first one, that can be inferred by the second, both in variable declarations and in theorem/definition assumptions. A regex search has been performed on the library to search for all occurrences and none is left.

Estimated changes

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

modified theorem Ideal.FinrankQuotientMap.linearIndependent_of_nontrivial

modified theorem Ideal.finrank_prime_pow_ramificationIdx

modified theorem Ideal.finrank_quotient_map

modified theorem Ideal.quotientToQuotientRangePowQuotSucc_injective

modified theorem Ideal.quotientToQuotientRangePowQuotSucc_surjective

modified theorem Ideal.rank_pow_quot

modified theorem Ideal.rank_pow_quot_aux

modified theorem Ideal.rank_prime_pow_ramificationIdx

modified theorem Ideal.sum_ramification_inertia

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

deleted theorem FractionalIdeal.one_mem_inv_coe_ideal

modified theorem isDedekindDomain_iff_isDedekindDomainInv

added theorem one_mem_inv_coe_ideal

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

modified theorem IsDedekindDomain.isPrincipalIdealRing_localization_over_prime

modified theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime

modified theorem IsPrincipalIdealRing.of_finite_primes

Modified Mathlib/RingTheory/DedekindDomain/SInteger.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean