Commit 2026-04-17 15:37 82df3405

View on Github →

chore(RingTheory/DedekindDomain/Ideal/*): move decls into namespaces (#38133) There are a bunch of declarations in Mathlib.RingTheory.DedekindDomain.Ideal.{Basic|Lemmas} that are in the root namespace, but (I think) shouldn't be there. This PR moves them into the Ideal or the IsDedekindDomain (or FractionalIdeal, PrimeSpectrum in rare cases) namespaces (and does some minor cleanup). The old names are deprecated; this has the slightly unpleasant effect that the new ones cannot be used unqualified even when their name space is open (because then Lean thinks the name is ambiguous, even though it reeally isn't). See #Is there code for X? > Results on elements of number fields and ideals @ 💬.

Estimated changes

deleted theorem one_mem_inv_coe_ideal
modified theorem FractionalIdeal.inv_le_comm
modified theorem FractionalIdeal.le_inv_comm
modified theorem FractionalIdeal.sup_mul_inf
modified theorem Ideal.IsPrime.mem_pow_mul
modified theorem Ideal.IsPrime.mul_mem_pow
modified theorem Ideal.count_associates_eq'
modified theorem Ideal.count_associates_eq
modified theorem Ideal.dvd_span_singleton
modified theorem Ideal.iInf_mul
modified theorem Ideal.inf_mul
modified theorem Ideal.isPrime_of_prime
modified theorem Ideal.mul_iInf
modified theorem Ideal.mul_inf
modified theorem Ideal.pow_lt_self
modified theorem Ideal.pow_right_strictAnti
modified theorem Ideal.pow_succ_lt_pow
modified theorem Ideal.prime_iff_isPrime
modified theorem Ideal.prime_of_isPrime
deleted theorem coe_primesOverFinset
deleted theorem count_le_of_ideal_ge
deleted theorem irreducible_pow_sup
deleted theorem irreducible_pow_sup_of_ge
deleted theorem irreducible_pow_sup_of_le
deleted theorem map_prime_of_equiv
deleted theorem mem_primesOverFinset_iff
deleted theorem one_le_primesOver_ncard
deleted theorem primesOver_finite
deleted theorem primesOver_ncard_ne_zero
deleted theorem sup_eq_prod_inf_factors